Use abbrev instead of @[reducible] def which is same thing but shorter

Changes

1 changed files (+1/-2)

• Sort.lean
  • @@ -77,8 +77,7 @@ theorem ICan'tBelieveICanProveItCanSort : (ICan'tBelieveItCanSort.{0} A).Perm A
    ⟨perm A, sorted A⟩ -- Not sure why this needs so much boilerplate - @[reducible] - def le (a b : (ℕ × String)) := a.1 > b.1 ∨ (a.1 = b.1 ∧ a.2 ≤ b.2) + abbrev le (a b : (ℕ × String)) := a.1 > b.1 ∨ (a.1 = b.1 ∧ a.2 ≤ b.2) instance : LE (ℕ × String) where le := le