diff --git a/tests/lean/run/doNotation1.lean b/tests/lean/run/doNotation1.lean index 7c72b159ca..db561c2daa 100644 --- a/tests/lean/run/doNotation1.lean +++ b/tests/lean/run/doNotation1.lean @@ -32,8 +32,8 @@ set_option trace.Elab.definition true def h (x : Nat) : StateT Nat IO Nat := do s ← get; -a ← f; -- liftM inserted here -b ← g1 (1:Nat); -- liftM inserted here +a ← f; -- liftM inserted here +b ← g1 1; -- liftM inserted here let x := g2 b; IO.println b; pure (s+a)