opaque Lean.Meta.Grind.normExt : SimpExtension

inductive Lean.Meta.Grind.AttrKind : Type

• ematch (k : EMatchTheoremKind) : AttrKind
• cases (eager : Bool) : AttrKind
• intro : AttrKind
• infer : AttrKind
• ext : AttrKind
• symbol (prio : Nat) : AttrKind
• inj : AttrKind
• funCC : AttrKind
• norm (post inv : Bool) : AttrKind
• unfold : AttrKind

def Lean.Meta.Grind.getAttrKindCore (stx : Syntax) : CoreM AttrKind

Return theorem kind for stx of the form Attr.grindThmMod

Equations

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

def Lean.Meta.Grind.getAttrKindFromOpt (stx : Syntax) : CoreM AttrKind

Return theorem kind for stx of the form (Attr.grindMod)?

Equations

• Lean.Meta.Grind.getAttrKindFromOpt stx = if stx[1].isNone = true then pure Lean.Meta.Grind.AttrKind.infer else Lean.Meta.Grind.getAttrKindCore stx[1][0]

def Lean.Meta.Grind.throwInvalidUsrModifier {α : Type} : CoreM α

Equations

• Lean.Meta.Grind.throwInvalidUsrModifier = Lean.throwError (Lean.toMessageData "the modifier `usr` is only relevant in parameters for `grind only`")

@[reducible, inline]

abbrev Lean.Meta.Grind.ExtensionMap : Type

Equations

• Lean.Meta.Grind.ExtensionMap = Std.HashMap Lean.Name Lean.Meta.Grind.Extension

opaque Lean.Meta.Grind.extensionMapRef : IO.Ref ExtensionMap

def Lean.Meta.Grind.getExtension? (attrName : Name) : CoreM (Option Extension)

Equations

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

def Lean.Meta.Grind.registerAttr (attrName : Name) (ref : Name := by exact decl_name%) : IO Extension

Equations

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

opaque Lean.Meta.Grind.grindExt : Extension

opaque Lean.Meta.Grind.liaExt : Extension

Extension backing the @[lia] attribute. It uses the same recording mechanism as @[grind] (see registerAttr), but provides a separate, smaller E-matching lemma set that the lia tactic instantiates (e.g. Nat.max_def), without enabling the full @[grind] set.

def Lean.Meta.Grind.isGlobalSplit (declName : Name) : CoreM Bool

Returns true is declName is a builtin split or has been tagged with [grind] attribute.

Equations

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