Documentation

Lean.Meta.Tactic.Grind.EMatchTheoremParam

source
def Lean.Meta.Grind.getLocalTheoremAnchors (goal : Goal) :
GrindM (Array ExprWithAnchor)

Returns pairs (type, anchor) where type is the type of a local theorem, and anchor the anchor associated with it.

Equations
    Instances For
      source
      def Lean.Meta.Grind.getNumDigitsForLocalTheoremAnchors (goal : Goal) :
      GrindM Nat

      Returns the number of digits needed to distinguish between different anchors.

      Equations
        Instances For
          source
          def Lean.Meta.Grind.globalDeclToGrindParamSyntax (declName : Name) (kind : EMatchTheoremKind) (minIndexable : Bool) :
          MetaM (TSyntax `Lean.Parser.Tactic.grindParam)
          Equations
            Instances For
              source
              def Lean.Meta.Grind.globalDeclToInstantiateParamSyntax (declName : Name) (kind : EMatchTheoremKind) (minIndexable : Bool) :
              MetaM (TSyntax `Lean.Parser.Tactic.Grind.thm)
              Equations
                Instances For