Use recursive def actually because it's shorter but keep the inductive predicate commented

Changes

1 changed files (+10/-4)

• InsertionSort.lean
  • @@ -19,15 +19,21 @@ def sort : List α → List α
    | [] => [] | h :: t => sInsert h (sort t) - /-- Inductive predicate for a list being sorted -/ + /-- Predicate for a list being sorted -/ @[grind] + def sorted : List α → Prop + -- An empty list is sorted + | [] => True + -- A list containing a single element is sorted + | [_] => True + -- A list with 2 or more elements is only sorted if all elements are ordered. + | h1 :: h2 :: t => h1 ≤ h2 ∧ sorted (h2 :: t) + /- This also works: inductive sorted : List α → Prop where - -- An empty list is sorted | nil : sorted [] - -- A list containing a single element is sorted | single x : sorted [x] - -- A list with more than 2 elements is only sorted if all elements are ordered. | cons_cons x x' xs : x ≤ x' → sorted (x' :: xs) → sorted (x :: x' :: xs) + -/ variable (l : List α)