AST for proof context?

Stream: lean4

[Rehnertz]

I'm working on auto proving and want to get the context (premises and golas) in tactic mode. Is it possible? Is there any reference or tutorial to extract AST of the context?

[Henrik Böving]

You should read the lean 4 meta programming book:https://github.com/leanprover-community/lean4-metaprogramming-book

[Adam Topaz]

If you want a pretty printed representation of the context, there is a function called ppGoal or something like that. You could look at its implementation for some hints as well