Don't need to abbrev when already @[simp]ed

Changes

1 changed files (+1/-1)

• Enlightened.lean
  • @@ -2,7 +2,7 @@ @[simp]
    instance : LE α := ⟨fun _ _ ↦ True⟩ @[simp] - abbrev Sorted : List α → Prop + def Sorted : List α → Prop | [] | [_] => True | x :: x' :: xs => x ≤ x' ∧ Sorted (x' :: xs)