Slightly simplify the LE boilerplate

Changes

1 changed files (+1/-4)

• Sort.lean
  • @@ -82,9 +82,6 @@ def le (a : (ℕ × String)) (b : (ℕ × String)) := a.1 > b.1 ∨ (a.1 = b.1
    instance : LE (ℕ × String) where le := le - instance {a : (ℕ × String)} {b : (ℕ × String)} : Decidable (a ≤ b) := - inferInstanceAs (Decidable (le a b)) - @[grind] lemma le_def {a : (ℕ × String)} {b : (ℕ × String)} : a ≤ b ↔ le a b := .rfl
  • @@ -93,6 +90,6 @@ instance : LinearOrder (ℕ × String) where
    le_trans := by grind le_antisymm := by grind le_total := by grind - toDecidableLE := inferInstanceAs _ + toDecidableLE a b := inferInstanceAs <| Decidable <| le a b #eval ICan'tBelieveItCanSort #[(69, "hi"), (1729, "blah"), (13, "a"), (420, "a"), (420, "meow")]