ink

def Std.Tactic.showTermTac : Lean.ParserDescr

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.

ink

def Std.Tactic.showTerm : Lean.ParserDescr

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