40e8f4c5fb
This PR turns on the new `do` elaborator in Init, Lean, Std, Lake and the testsuite. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
14 lines
398 B
Text
14 lines
398 B
Text
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))
|