show_term tac
runs tac
, then prints the generated term in the form
"exact X Y Z" or "refine X ?_ Z" if there are remaining subgoals.
(For some tactics, the printed term will not be human readable.)
Instances For
show_term e
elaborates e
, then prints the generated term.
(For some tactics, the printed term will not be human readable.)
Instances For
The command by?
will print a suggestion for replacing the proof block with a proof term
using show_term
.