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

def Std.Tactic.showTermImpl : Lean.ParserDescr

Implementation of show_term.

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

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.