def Lean.Meta.Grind.getFunCCSet : CoreM NameSet

Equations

• Lean.Meta.Grind.getFunCCSet = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Grind.funCCExt✝ __do_lift)

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

Equations

• Lean.Meta.Grind.hasFunCCAttr declName = do let __do_lift ← Lean.Meta.Grind.getFunCCSet pure (__do_lift.contains declName)

def Lean.Meta.Grind.addFunCCAttr (declName : Name) (attrKind : AttributeKind) : CoreM Unit

Equations

• Lean.Meta.Grind.addFunCCAttr declName attrKind = Lean.ScopedEnvExtension.add Lean.Meta.Grind.funCCExt✝ declName attrKind

def Lean.Meta.Grind.eraseFunCCAttr (declName : Name) : CoreM Unit

Equations

• One or more equations did not get rendered due to their size.