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

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-10 14:48:57 -08:00
parent d37eb896ef
commit 34776c4f41
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/run/coroutine.lean
View file

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