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.

def Std.Tactic.showTermImpl : Lean.ParserDescr

Implementation of show_term.

Equations

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

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

def Std.Tactic.by? : Lean.ParserDescr

The command by? will print a suggestion for replacing the proof block with a proof term using show_term.

Equations

• Std.Tactic.by? = Lean.ParserDescr.node `Std.Tactic.by? 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "by?") (Lean.ParserDescr.const `tacticSeq))