test: monad stack with multiple ExceptT
cc @Kha :)
This commit is contained in:
parent
8a6cb1842f
commit
f6fffc9532
1 changed files with 29 additions and 0 deletions
29
tests/lean/run/doNotation5.lean
Normal file
29
tests/lean/run/doNotation5.lean
Normal file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue