opaque Lean.Meta.Grind.grindNormExt : Lean.Meta.SimpExtension

opaque Lean.Meta.Grind.grindNormSimprocExt : Lean.Meta.Simp.SimprocExtension

opaque Lean.Meta.Grind.grindCasesExt : Lean.SimpleScopedEnvExtension Lean.Name Lean.NameSet

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

Returns true if declName has been tagged with attribute [grind_cases].