@[instance]
Equations
- ordering.has_repr = {repr := λ (s : ordering), ordering.has_repr._match_1 s}
- ordering.has_repr._match_1 ordering.gt = "gt"
- ordering.has_repr._match_1 ordering.eq = "eq"
- ordering.has_repr._match_1 ordering.lt = "lt"
Equations
Equations
- ordering.gt.or_else _x = ordering.gt
- ordering.eq.or_else o = o
- ordering.lt.or_else _x = ordering.lt
Equations
- cmp_using lt a b = ite (lt a b) ordering.lt (ite (lt b a) ordering.gt ordering.eq)
@[instance]
Equations
- ordering.decidable_eq = λ (a b : ordering), ordering.decidable_eq._match_1 b a
- ordering.decidable_eq._match_1 b ordering.gt = ordering.decidable_eq._match_4 b
- ordering.decidable_eq._match_1 b ordering.eq = ordering.decidable_eq._match_3 b
- ordering.decidable_eq._match_1 b ordering.lt = ordering.decidable_eq._match_2 b
- ordering.decidable_eq._match_4 ordering.gt = decidable.is_true rfl
- ordering.decidable_eq._match_4 ordering.eq = decidable.is_false ordering.decidable_eq._match_4._proof_2
- ordering.decidable_eq._match_4 ordering.lt = decidable.is_false ordering.decidable_eq._match_4._proof_1
- ordering.decidable_eq._match_3 ordering.gt = decidable.is_false ordering.decidable_eq._match_3._proof_2
- ordering.decidable_eq._match_3 ordering.eq = decidable.is_true rfl
- ordering.decidable_eq._match_3 ordering.lt = decidable.is_false ordering.decidable_eq._match_3._proof_1
- ordering.decidable_eq._match_2 ordering.gt = decidable.is_false ordering.decidable_eq._match_2._proof_2
- ordering.decidable_eq._match_2 ordering.eq = decidable.is_false ordering.decidable_eq._match_2._proof_1
- ordering.decidable_eq._match_2 ordering.lt = decidable.is_true rfl