From f6fffc9532f832fc2ebdc8350a57eb52a5f683a3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Oct 2020 19:53:12 -0700 Subject: [PATCH] test: monad stack with multiple `ExceptT` cc @Kha :) --- tests/lean/run/doNotation5.lean | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 tests/lean/run/doNotation5.lean diff --git a/tests/lean/run/doNotation5.lean b/tests/lean/run/doNotation5.lean new file mode 100644 index 0000000000..2572b08e9a --- /dev/null +++ b/tests/lean/run/doNotation5.lean @@ -0,0 +1,29 @@ +new_frontend + +abbrev M := ExceptT String $ ExceptT Nat $ StateM Nat + +def inc (x : Nat) : M Unit := do +if (← get) >= 100 then + throwThe Nat ((← get) + x) +modify (· + x) + +def dec (x : Nat) : M Unit := do +if (← get) - x == 0 then + throw "balance is zero" +modify (· - x) + +def f (x y : Nat) : M Nat := do +try + inc x + dec y + get +catch ex : String => + dbgTrace! "string exception " ++ toString ex + pure 1000 +catch ex : Nat => + dbgTrace! "nat exception " ++ toString ex + pure ex + +#eval (f 10 20).run 1000 +#eval (f 10 200).run 10 +#eval (f 10 20).run 30