access raw proof terms

Stream: Is there code for X?

[Andre Graubner (安德)]

Andre Graubner (安德) 1:30 PM
Hello, I hope this is the right place to ask this. I'm curious if there's a way to look at 'raw proof terms' as constructed by using tactics. I'm a bit new to this so I might be misunderstanding something, but can I somehow get the low-level, functional lean code from a higher-level proof? To give some context, I'm interested in pattern mining and analysis of proofs in lean, and for that I would like to explore what existing ways there are to actually access things like syntax trees for existing lean code. I'm not quite sure what I would be searching for in order to find this on google... Thanks!

[Junyan Xu]

You can encircle the tactics by show_term { }, or use #print, for example

import tactic.norm_num
lemma test : 2 + 3 = 5 := by show_term { norm_num }
#print test

[Andre Graubner (安德)]

I'll try this, thank you very much.

[Junyan Xu]

You may also want to read this and maybe the proof artifact co-training paper.

[Andre Graubner (安德)]

Thanks, I just came across that paper as well and it seems very relevant. Thank you!

[Meow]

Why #print is unable to use in Lean 3?