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

• One or more equations did not get rendered due to their size.

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

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

Equations

• Lean.Meta.Grind.getNumDigitsForLocalTheoremAnchors goal = do let __do_lift ← Lean.Meta.Grind.getLocalTheoremAnchors goal pure (Lean.Meta.Grind.getNumDigitsForAnchors __do_lift)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.