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