From 362185147e6ce561cbcb6a264ed7128f6f7acd76 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Feb 2020 14:21:26 -0800 Subject: [PATCH] chore: remove unncessary annotation --- tests/lean/run/doNotation1.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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)