How to view the proof term generated by a tactic?

Stream: new members

[Michael Fishman]

I want to view the proof term generated by a tactic.

I thought show_term may have done this, but in the example I tried, replacing rfl with the output of show_term rfl, exact Eq.refl my_sum, did not give a valid proof.

[Mirek Olšák]

#print my_theorem_name

[Kyle Miller]

That's not going to be appreciably different @Mirek Olšák. It uses the same mechanism as show_term, the pretty printer.

[Kyle Miller]

@Michael Fishman Pretty printing isn't guaranteed to round-trip, which can be unfortunate for this use case, but you can try adding flags like set_option pp.explicit true, or more strongly set_option pp.all true. There are other options too.

[Mirek Olšák]

If the issue is that the irreducible constants are not expanded by the elaborator, it is an "issue" of the elaborator, and not a proof not being valid.

[Mirek Olšák]

For example

example : 1 + 1 = (2 : ℚ) := @Eq.refl.{1} ℚ 2

is a valid proof term. Kernel would accept it if there was not for the high-level type checker that errors out because it doesn't expand Rat.add (and there are ways to convince the elaborator without changing the term).