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