diff --git a/tests/lean/run/LiftMethodIssue.lean b/tests/lean/run/LiftMethodIssue.lean index b5fb7d7f21..3f47de2079 100644 --- a/tests/lean/run/LiftMethodIssue.lean +++ b/tests/lean/run/LiftMethodIssue.lean @@ -6,7 +6,7 @@ pure x? def tst2 (x : Nat) : IO (Option Nat) := do x? : Option Nat ← pure x; -if x?.isNone then +(if x?.isNone then /- We need the `some` because we propagate the expected type at `pure` applications. The expected type is `IO (Option Nat)`, and we elaborate `x+1` with expected type @@ -17,4 +17,4 @@ if x?.isNone then -/ pure $ some (x+1) else - pure x? + pure x?) diff --git a/tests/lean/run/array1.lean b/tests/lean/run/array1.lean index d8e04cfe8d..3d643f059a 100644 --- a/tests/lean/run/array1.lean +++ b/tests/lean/run/array1.lean @@ -45,7 +45,7 @@ def tst1 : IO Unit := def tst : IO (List Nat) := [1, 2, 3, 4].filterMapM fun x => do IO.println x; - if x % 2 == 0 then pure $ some (x + 10) else pure none + (if x % 2 == 0 then pure $ some (x + 10) else pure none) #eval tst diff --git a/tests/lean/run/doNotation1.lean b/tests/lean/run/doNotation1.lean index 5175d07a16..4cf7035413 100644 --- a/tests/lean/run/doNotation1.lean +++ b/tests/lean/run/doNotation1.lean @@ -71,21 +71,21 @@ IO.println "hello"; IO.println x def tst3 : IO Unit := do -if (← g 1) > 0 then +(if (← g 1) > 0 then IO.println "gt" else do x ← f; y ← g x; - IO.println y; + IO.println y) def pred (x : Nat) : IO Bool := do pure $ (← g x) > 0 def tst4 (x : Nat) : IO Unit := do -if ← pred x then +(if ← pred x then IO.println "is true" else do - IO.println "is false" + IO.println "is false") def pred2 (x : Nat) : IO Bool := pure $ x > 0 @@ -109,15 +109,15 @@ partial def expandHash : Syntax → StateT Bool MacroM Syntax @[macro Lean.Parser.Term.do] def expandDo : Macro := fun stx => do (stx, expanded) ← expandHash stx false; - if expanded then pure stx - else Macro.throwUnsupported + (if expanded then pure stx + else Macro.throwUnsupported) def tst7 : StateT (Nat × Nat) IO Unit := do -if #.1 == 0 then +(if #.1 == 0 then IO.println "first field is zero" else - IO.println "first field is not zero" + IO.println "first field is not zero") #check tst7