max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove unncessary annotation

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-04 14:21:26 -08:00
parent b5eb64da3a
commit 362185147e
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/run/doNotation1.lean
View file

@ -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)