Documentation

Lean.Data.Name

source
@[export lean_name_hash_exported]
def Lean.Name.hashEx :
Name → UInt64
Equations
source
def Lean.Name.getPrefix :
Name → Name
Equations
source
def Lean.Name.getString! :
Name → String
Equations
source
def Lean.Name.getNumParts :
Name → Nat
Equations
source
def Lean.Name.updatePrefix :
Name → Name → Name
Equations
source
def Lean.Name.componentsRev :
Name → List Name
Equations
source
def Lean.Name.components (n : Name) :
List Name
Equations
source
def Lean.Name.eqStr :
Name → String → Bool
Equations
source
def Lean.Name.isPrefixOf :
Name → Name → Bool
Equations
source
def Lean.Name.isSuffixOf :
Name → Name → Bool
Equations
source
def Lean.Name.cmp :
Name → Name → Ordering
Equations
source
def Lean.Name.lt (x y : Name) :
Bool
Equations
source
def Lean.Name.quickCmpAux :
Name → Name → Ordering
Equations
Instances For
source
def Lean.Name.quickCmp (n₁ n₂ : Name) :
Ordering
Equations
Instances For
source
def Lean.Name.quickLt (n₁ n₂ : Name) :
Bool
Equations
source
def Lean.Name.hasNum :
Name → Bool

Returns true if the name has any numeric components.

Equations
source
def Lean.Name.isInternal :
Name → Bool

The frontend does not allow user declarations to start with _ in any of its parts. We use name parts starting with _ internally to create auxiliary names (e.g., _private).

Equations
source
def Lean.Name.isInternalOrNum :
Name → Bool

The frontend does not allow user declarations to start with _ in any of its parts. We use name parts starting with _ internally to create auxiliary names (e.g., _private).

This function checks if any component of the name starts with _, or is numeric.

Equations
source
def Lean.Name.isInternalDetail :
Name → Bool

Returns true if this a part of name that is internal or dynamically generated so that it may easily be changed.

Generally, user code should not explicitly use internal names.

Equations
source
def Lean.Name.isInternalDetail.matchPrefix (s pre : String) :
Bool

Check that a string begins with the given prefix, and then is only digit characters.

Equations
source
def Lean.Name.isImplementationDetail :
Name → Bool

Checks whether the name is an implementation-detail hypothesis name.

Implementation-detail hypothesis names start with a double underscore.

Equations
source
def Lean.Name.isAtomic :
Name → Bool
Equations
source
def Lean.Name.isAnonymous :
Name → Bool
Equations
source
def Lean.Name.isStr :
Name → Bool
Equations
source
def Lean.Name.isNum :
Name → Bool
Equations
source
def Lean.Name.anyS (n : Name) (f : String → Bool) :
Bool

Return true if n contains a string part s that satisfies f.

Examples:

#eval (`foo.bla).anyS (·.startsWith "fo") -- true
#eval (`foo.bla).anyS (·.startsWith "boo") -- false
Equations