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

Equations

• Lean.Meta.Grind.getExtension? attrName = do let __do_lift ← ST.Ref.get Lean.Meta.Grind.extensionMapRef pure __do_lift[attrName]?

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

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.