inductive Lean.Meta.Grind.AttrKind : Type

• ematch (k : EMatchTheoremKind) : AttrKind
• cases (eager : Bool) : AttrKind
• intro : AttrKind
• infer : AttrKind
• ext : 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`")