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

Instances For

    Implementation of show_term.

    Instances For

      show_term e elaborates e, then prints the generated term.

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

      Instances For

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

        Instances For