source
opaque Lean.protectedExt :
TagDeclarationExtension
source
def Lean.addProtected (env : Environment) (n : Name) :
Environment
Equations

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

Instances For

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

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

Instances For

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

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

Instances For