← Copula mathematical handbook

opaque Lean.protectedExt : TagDeclarationExtension

def Lean.addProtected (env : Environment) (n : Name) : Environment

Equations

• Lean.addProtected env n = Lean.protectedExt.tag env n

def Lean.isProtected (env : Environment) (n : Name) : Bool

Equations

• Lean.isProtected env n = Lean.protectedExt.isTagged env n

def Lean.mkPrivateName (env : Environment) (n : Name) : Name

Equations

• Lean.mkPrivateName env n = Lean.mkPrivateNameCore env.mainModule (Lean.privateToUserName n)