Don't need to return in identity monad

Changes

2 changed files (+2/-2)

• Kadane.lean
  • @@ -7,7 +7,7 @@ def kadane (A : Array ℤ) := Id.run do
    for x in A do cur := max x (cur + x) ans := max ans cur - return ans + ans def is_max_nonempty_suffix (xs : List ℤ) m := (∃ i ≤ xs.length, (xs.drop i).sum = m) ∧ ∀ i < xs.length, (xs.drop i).sum ≤ m
• Sort.lean
  • @@ -11,7 +11,7 @@ def ICan'tBelieveItCanSort := Id.run do
    for hj : j in [:N] do if A[i] < A[j] then A := A.swap i j - return A.toArray + A.toArray #guard let A := #[69, 420, 1, 1, 13, 1, 65536] ICan'tBelieveItCanSort A = A.qsort