Reformat InsertionSort.lean

Changes

1 changed files (+6/-6)

• InsertionSort.lean
  • @@ -22,12 +22,12 @@ def sort : List α → List α
    /-- 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) + -- 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 | nil : sorted []