# 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.

source
def Lean.privateHeader :
Name
Equations

- Lean.privateHeader = `_private

Instances For

source
def Lean.mkPrivateNameCore (mainModule n : Name) :
Name
Equations

- Lean.mkPrivateNameCore mainModule n = (Lean.privateHeader ++ mainModule).mkNum 0 ++ n

Instances For

source
def Lean.isPrivateName :
Name → Bool
Equations

- Lean.isPrivateName (p.str str) = (p.str str == Lean.privateHeader || Lean.isPrivateName p)
- Lean.isPrivateName (p.num i) = Lean.isPrivateName p
- Lean.isPrivateName x✝ = false

Instances For

source
@[export lean_is_private_name]
def Lean.isPrivateNameExport (n : Name) :
Bool
Equations

- Lean.isPrivateNameExport n = Lean.isPrivateName n

Instances For

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

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

Equations

- Lean.isPrivatePrefix (p.num 0) = Lean.isPrivatePrefix.go✝ p
- Lean.isPrivatePrefix n = false

Instances For

source
@[export lean_private_to_user_name]
def Lean.privateToUserName? (n : Name) :
Option Name
Equations

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

Instances For

source
def Lean.privateToUserName (n : Name) :
Name
Equations

- Lean.privateToUserName n = if Lean.isPrivateName n = true then Lean.privateToUserNameAux✝ n else n

Instances For

source
@[export lean_private_prefix]
def Lean.privatePrefix? (n : Name) :
Option Name
Equations

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

Instances For