Oh don't need parens for fun in DiabolicalSort

Changes

1 changed files (+1/-1)

• BadSort.lean
  • @@ -8,6 +8,6 @@ def BadSort [LinearOrder α] (A : List α)
    def WorstSort [LinearOrder α] (A : List α) (f : ℕ → ℕ) := BadSort A <| f A.length - def DiabolicalSort [LinearOrder α] (A : List α) := WorstSort A (fun n ↦ ack n n) + def DiabolicalSort [LinearOrder α] (A : List α) := WorstSort A fun n ↦ ack n n -- Probably not to hard to prove that this is correct but left as an exercise to the reader