opaque Lean.protectedExt : Lean.TagDeclarationExtension

@[export lean_add_protected]

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

Equations

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

@[export lean_is_protected]

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

Equations

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

Private name support.

Suppose the user marks as declaration n as private. Then, we create the name: _private.<module_name>.0 ++ n. We say _private.<module_name>.0 is the "private prefix"

We assume that n is a valid user name and does not contain Name.num constructors. Thus, we can easily convert from private internal name to the user given name.

def Lean.privateHeader : Lake.Name

Equations

• Lean.privateHeader = `_private

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

Equations

• Lean.mkPrivateName env n = Lean.Name.mkNum (Lean.privateHeader ++ Lean.Environment.mainModule env) 0 ++ n

def Lean.isPrivateName : Lake.Name → Bool

Equations

• Lean.isPrivateName (Lean.Name.str p str) = (Lean.Name.str p str == Lean.privateHeader || Lean.isPrivateName p)
• Lean.isPrivateName (Lean.Name.num p i) = Lean.isPrivateName p
• Lean.isPrivateName x = false

@[export lean_is_private_name]

def Lean.isPrivateNameExport (n : Lake.Name) : Bool

Equations

• Lean.isPrivateNameExport n = Lean.isPrivateName n

def Lean.isPrivatePrefix (n : Lake.Name) : Bool

Return true if n is of the form _private.<module_name>.0 See comment above.

Equations

• Lean.isPrivatePrefix n = match n with | Lean.Name.num p 0 => Lean.isPrivatePrefix.go p | x => false

def Lean.isPrivatePrefix.go (n : Lake.Name) : Bool

Equations

• Lean.isPrivatePrefix.go (Lean.Name.str p str) = (Lean.Name.str p str == Lean.privateHeader || Lean.isPrivatePrefix.go p)
• Lean.isPrivatePrefix.go n = (n == Lean.privateHeader || false)

@[export lean_private_to_user_name]

def Lean.privateToUserName? (n : Lake.Name) : Option Lake.Name

Equations

• Lean.privateToUserName? n = if Lean.isPrivateName n = true then some (Lean.privateToUserNameAux n) else none

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

Equations

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

@[export lean_private_prefix]

def Lean.privatePrefix? (n : Lake.Name) : Option Lake.Name

Equations

• Lean.privatePrefix? n = if Lean.isPrivateName n = true then some (Lean.privatePrefixAux n) else none