# Documentation

Std.Tactic.ShowTerm

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.)

Equations
• One or more equations did not get rendered due to their size.

show_term e elaborates e, then prints the generated term.

(For some tactics, the printed term will not be human readable.)

Equations