Revert "Don't need to return in identity monad" This reverts commit 9baf7fc0daca8a230f11512125ef663a5d60f801.

Changes

2 changed files (+2/-2)

• Conventional.lean
  • @@ -9,7 +9,7 @@ if A[i - j]'(by sorry) < A[i - j - 1]'(by sorry) then
    A := A.swap (i - j - 1) (i - j) (by sorry) (by sorry) else break - A + return A -- Obviously that code is correct theorem insSortCorrect : True := .intro
• Imperative.lean
  • @@ -12,7 +12,7 @@ if A[i - j] < A[i - j - 1] then
    A := A.swap (i - j - 1) (i - j) else break - A.toArray + return A.toArray open Std.Do