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
    Instances For
      source
      def Lean.Elab.Tactic.elabShow.go (newType : Term) (firstGoal : MVarId) (goals prevRev : List MVarId) :
      TacticM Unit
      Equations
        Instances For
          source
          def Lean.Elab.Tactic.elabShow.tryGoal (newType : Term) (goal : MVarId) (goals prevRev : List MVarId) (err : Expr → Expr → MetaM MessageData) :
          TacticM Unit
          Equations
            Instances For
              source
              def Lean.Elab.Tactic.elabShow.simpleError (p tgt : Expr) :
              MetaM MessageData
              Equations
                Instances For
                  source
                  def Lean.Elab.Tactic.elabShow.manyError (p tgt : Expr) :
                  MetaM MessageData
                  Equations
                    Instances For