From 34776c4f41ebe329fbe3065add6b0aa0397ec9aa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 10 Feb 2020 14:48:57 -0800 Subject: [PATCH] chore: fix test --- tests/lean/run/coroutine.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/tests/lean/run/coroutine.lean b/tests/lean/run/coroutine.lean index 3f4963860e..ad47b73df7 100644 --- a/tests/lean/run/coroutine.lean +++ b/tests/lean/run/coroutine.lean @@ -162,8 +162,8 @@ unsafe def visit {α : Type v} : tree α → coroutine Unit α Unit unsafe def tst {α : Type} [HasToString α] (t : tree α) : ExceptT String IO Unit := do c ← pure $ visit t; - (yielded v₁ c) ← pure $ resume c (); - (yielded v₂ c) ← pure $ resume c (); + (yielded v₁ c) ← pure (resume c ()) | throw "failed"; + (yielded v₂ c) ← pure (resume c ()) | throw "failed"; IO.println $ toString v₁; IO.println $ toString v₂; pure () @@ -187,12 +187,12 @@ do unsafe def tst2 : ExceptT String IO Unit := do let c := StateT.run ex 5; - (yielded r c₁) ← pure $ resume c 10; + (yielded r c₁) ← pure $ resume c 10 | throw "failed"; IO.println r; - (yielded r c₂) ← pure $ resume c₁ 20; + (yielded r c₂) ← pure $ resume c₁ 20 | throw "failed"; IO.println r; - (done _) ← pure $ resume c₂ 30; - (yielded r c₃) ← pure $ resume c₁ 100; + (done _) ← pure $ resume c₂ 30 | throw "failed"; + (yielded r c₃) ← pure $ resume c₁ 100 | throw "failed"; IO.println r; IO.println "done"; pure ()