opaque Lean.protectedExt : TagDeclarationExtension

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

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

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

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