@[export lean_add_protected]
Equations
Instances For
@[export lean_is_protected]
Equations
Instances For
Private name support. #
Suppose the user marks as declaration n
as private. Then, we create
the name: _private.
.
We say _private.
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.
Equations
- Lean.mkPrivateName env n = Lean.Name.mkNum (Lean.privateHeader ++ Lean.Environment.mainModule env) 0 ++ n
Instances For
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
Instances For
@[export lean_is_private_name]
Equations
Instances For
@[export lean_private_to_user_name]
Equations
- Lean.privateToUserName? n = if Lean.isPrivateName n = true then some (Lean.privateToUserNameAux n) else none
Instances For
Equations
- Lean.isPrivateNameFromImportedModule env n = match Lean.privateToUserName? n with | some userName => Lean.mkPrivateName env userName != n | x => false
Instances For
@[export lean_private_prefix]
Equations
- Lean.privatePrefix? n = if Lean.isPrivateName n = true then some (Lean.privatePrefixAux n) else none