Zulip Chat Archive
Stream: lean4
Topic: Derived Ord instance
Chris B (Dec 27 2021 at 03:55):
The derive handler for Ord
currently compares fields from the bottom up. Is this intended or is it a bug?
structure Color where
r : Nat
g : Nat
b : Nat
deriving Ord
/-
[Elab.Deriving.ord]
[mutual
private def ordColor✝ (x✝ : @Time.Color) (x✝¹ : @Time.Color) : Ordering✝ :=
match x✝, x✝¹ with
| @Time.Color.mk a✝ a✝¹ a✝², @Time.Color.mk b✝ b✝¹ b✝² =>
match compare✝ a✝² b✝² with
| Ordering.lt✝ => Ordering.lt✝
| Ordering.gt✝ => Ordering.gt✝
| Ordering.eq✝ =>
match compare✝ a✝¹ b✝¹ with
| Ordering.lt✝ => Ordering.lt✝
| Ordering.gt✝ => Ordering.gt✝
| Ordering.eq✝ =>
match compare✝ a✝ b✝ with
| Ordering.lt✝ => Ordering.lt✝
| Ordering.gt✝ => Ordering.gt✝
| Ordering.eq✝ => Ordering.eq✝
end,
instance : Ord (@Time.Color) :=
⟨ordColor✝⟩]
-/
Last updated: Dec 20 2023 at 11:08 UTC