Expression printed as AST

Stream: Is there code for X?

[Xavier Martinet]

Hi everyone! I am pretty new to Lean, and I was wondering: is there any way to get the underlying ASTs behind the mathematical expression manipulated by Lean? For instance I saw there was a set_option pp.notation false I could parse, but maybe there was a better way to automatically extract the AST directly?

[Scott Morrison]

See if lean --make --ast foo.lean gives you something you like.

[Scott Morrison]

(This exists solely to support migrating mathlib to lean4, so if it's not what you're after the alternative answer is to switch to lean4.)

[Mario Carneiro]

lean --ast is good for if you want to manipulate the AST of a lean expression outside of lean. If you want the AST inside lean, you can just parse it into an expr and pattern match on it, print it using tactic.pp and other things

[Xavier Martinet]

Thanks! I will try that