import Lean.Hygiene import Lean.Exception set_option backward.do.legacy false open Lean def bar : StateT Nat Unhygienic Syntax.Term := do modify (ยท + 1); `("hi") def foo : StateT Nat Unhygienic Syntax.Term := do `(throwError $(โ† bar)) #eval Unhygienic.run (foo.run 0) |>.2 -- don't do this syntax "โ†" term : term def foo' : StateT Nat Unhygienic Syntax.Term := do `(throwError $(โ† bar))