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

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) : IO (Option Extension)

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

opaque Lean.Meta.Grind.grindExt : Extension

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

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