| abbrev M := ReaderT String $ StateT Nat $ ReaderT Bool $ IO | |
| def f : M Nat := do | |
| let s ← read | |
| IO.println s | |
| let b ← readThe Bool | |
| IO.println b | |
| let s ← get | |
| pure s | |
| /-- | |
| info: hello | |
| true | |
| --- | |
| info: 10 | |
| -/ | |
| #guard_msgs in | |
| #eval (f "hello").run' 10 true | |
| def g : M Nat := | |
| let a : M Nat := withTheReader Bool not f | |
| withReader (fun s => s ++ " world") a | |
| /-- | |
| info: hello world | |
| false | |
| --- | |
| info: 10 | |
| -/ | |
| #guard_msgs in | |
| #eval (g "hello").run' 10 true |