| macroStack.lean:4:5-4:6: error: unknown identifier 'x' | |
| macroStack.lean:8:6-8: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:11:9-11:15: error: invalid use of `(<- ...)`, must be nested inside a 'do' expression | |
| macroStack.lean:17:0-17:6: error: failed to synthesize | |
| HAdd Nat String ?m | |
| Additional diagnostic information may be available using the `set_option diagnostics 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 |