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
• homo : AttrKind
• homoPred : AttrKind

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

Return theorem kind for stx of the form Attr.grindThmMod

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

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

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

@[reducible, inline]

abbrev Lean.Meta.Grind.ExtensionMap : Type

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

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

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

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.