Documentation

Lean.Elab.Tactic.Show

Implementation of the show tactic #

The show p tactic finds the first goal that p unifies with and brings it to the front of the goal list. If there were a first_goal combinator, it would be like first_goal change p.

source
def Lean.Elab.Tactic.elabShow (newType : Term) :
TacticM Unit
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Elab.Tactic.evalShow :
    Tactic
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For