From 4a2a2758ec8da9dbc9965255e42d391b875117ec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 4 Oct 2020 16:19:50 -0700 Subject: [PATCH] chore: adjust test --- tests/lean/run/monadControl.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/monadControl.lean b/tests/lean/run/monadControl.lean index ffc53982d8..2b1971b464 100644 --- a/tests/lean/run/monadControl.lean +++ b/tests/lean/run/monadControl.lean @@ -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