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
- Std.Tactic.showTerm = Lean.ParserDescr.node `Std.Tactic.showTerm 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "show_term ") (Lean.ParserDescr.cat `term 0))