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>
27 lines
868 B
Text
27 lines
868 B
Text
macroStack.lean:5:5-5:6: error(lean.unknownIdentifier): Unknown identifier `x`
|
|
macroStack.lean:9:6-9:7: error: Unknown identifier `x`
|
|
with resulting expansion
|
|
binrel% GT.gt✝ x 0
|
|
while expanding
|
|
x > 0
|
|
while expanding
|
|
(x > 0)
|
|
while expanding
|
|
if h : (x > 0) then 1 else 0
|
|
macroStack.lean:12:9-12:15: error: Nested action `← get` must be nested inside a `do` expression.
|
|
macroStack.lean:18:0-18:6: error: failed to synthesize instance of type class
|
|
HAdd Nat String ?m
|
|
|
|
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
|
|
with resulting expansion
|
|
binop% HAdd.hAdd✝ (x + x✝) x✝¹
|
|
while expanding
|
|
(x + x✝) + x✝¹
|
|
while expanding
|
|
foo!(x + x✝)
|
|
while expanding
|
|
foo!(x + x✝) < 1
|
|
while expanding
|
|
if foo!(x + x✝) < 1 then true✝ else false✝
|
|
while expanding
|
|
bla! x
|