Documentation

Lean.Modifiers

opaque Lean.protectedExt:

Lean.TagDeclarationExtension

@[export lean_add_protected]

def Lean.addProtected (env : Lean.Environment) (n : Lean.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 : Lean.Name) :

Equations

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

def Lean.privateHeader:

Equations

Lean.privateHeader = `_private

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

Equations

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

def Lean.isPrivateName:

Lean.Name → Bool

Equations

Lean.isPrivateName (Lean.Name.str p a a_1) = (Lean.Name.str p a a_1 == Lean.privateHeader || Lean.isPrivateName p)
Lean.isPrivateName (Lean.Name.num p a a_1) = Lean.isPrivateName p
Lean.isPrivateName _fun_discr = false

@[export lean_is_private_name]

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

Equations

Lean.isPrivateNameExport n = Lean.isPrivateName n

@[export lean_private_to_user_name]

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

Option Lean.Name

Equations

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

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

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 : Lean.Name) :

Option Lean.Name

Equations

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