chore: restore accidentally deleted test

25447af13c
This commit is contained in:
Leonardo de Moura 2022-09-01 06:06:03 -07:00
parent c201133d4d
commit d96bf8a633

4
tests/lean/run/1547.lean Normal file
View file

@ -0,0 +1,4 @@
def foo (x : {_ : Unit} → StateM Nat Nat) : Nat :=
(@x () 0).1
def bar := foo (return 42)