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.privateHeader ++ env.mainModule).mkNum 0 ++ Lean.privateToUserName n

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

Equations

• Lean.isPrivateNameFromImportedModule env n = match Lean.privateToUserName? n with | some userName => Lean.mkPrivateName env userName != n | x => false