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

chore: adjust test

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-04 16:19:50 -07:00
parent 9810b405d9
commit 4a2a2758ec
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/monadControl.lean
View file

@ -26,7 +26,7 @@ let a ← x s.length;
IO.println ("ended");
pure a
@[inline] def g' {α m} [MonadControlT IO m] [HasBind m] (msg : String) (x : Nat → m α) : m α := do
@[inline] def g' {α m} [MonadControlT IO m] [Monad m] (msg : String) (x : Nat → m α) : m α := do
controlAt IO fun runInBase => g msg (fun n => runInBase (x n))
def tst2 : M Nat := do