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.elabShow.go (newType : Term) (firstGoal : MVarId) (goals prevRev : List MVarId) :
    TacticM Unit
    Equations
    • One or more equations did not get rendered due to their size.
    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
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Elab.Tactic.elabShow.simpleError (p tgt : Expr) :
        MetaM MessageData
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Elab.Tactic.elabShow.manyError (p tgt : Expr) :
          MetaM MessageData
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For