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

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

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

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

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

Equations

• Lean.Meta.Grind.isGrindCasesTarget declName = do let __do_lift ← Lean.getEnv pure ((Lean.ScopedEnvExtension.getState Lean.Meta.Grind.grindCasesExt __do_lift).contains declName)