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 : Name

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

def Lean.isPrivateName : Name → Bool

@[export lean_is_private_name]

def Lean.isPrivateNameExport (n : Name) : Bool

def Lean.isPrivatePrefix (n : Name) : Bool

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

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

@[export lean_private_to_user_name]

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

def Lean.privateToUserName (n : Name) : Name

@[export lean_private_prefix]

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