Documentation

Lean.Modifiers

constant Lean.protectedExt :

Lean.TagDeclarationExtension

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

Lean.Environment

Equations

Lean.addProtected env n = Lean.TagDeclarationExtension.tag Lean.protectedExt env n

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 x_1 x_2) = (Lean.Name.str p x_1 x_2 == Lean.privateHeader || Lean.isPrivateName p)
Lean.isPrivateName (Lean.Name.num p x_1 x_2) = Lean.isPrivateName p
Lean.isPrivateName x = false

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

Equations

Lean.isPrivateNameExport n = Lean.isPrivateName n

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

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