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.

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

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

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