# Documentation

Lean.Modifiers

Equations
@[export lean_is_protected]
Equations

# Private name support. #

Suppose the user marks as declaration n as private. Then, we create the name: _private..0 ++ n. We say _private..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.

Equations
@[export lean_is_private_name]
Equations
@[export lean_private_to_user_name]
Equations
• = if then else none
Equations
@[export lean_private_prefix]
Equations
• = if then else none