Can I squeeze finish?

Stream: new members

[Martin Dvořák]

As we have simp and squeeze_simp, is there a similar option for finish please? Or maybe, rather than printing a list of lemmata that were used, I would like to display the end part of the proof (that was just generated) as a term. Can I do it?

[Alex J. Best]

You can use tactic#show_term to see the term produced, but it will be very unreadable. You might be able to see the names of a couple of useful things, but in general due to the way finish works it is not really amenable to producing nice tactic scripts.

[Damiano Testa]

Also, my experience is that pasting the output of show_term will not work as a valid proof.