@[export lean_name_hash_exported]

def Lean.Name.hashEx : Name → UInt64

def Lean.Name.getPrefix : Name → Name

def Lean.Name.getString! : Name → String

def Lean.Name.getNumParts : Name → Nat

def Lean.Name.updatePrefix : Name → Name → Name

def Lean.Name.componentsRev : Name → List Name

def Lean.Name.components (n : Name) : List Name

def Lean.Name.eqStr : Name → String → Bool

def Lean.Name.isPrefixOf : Name → Name → Bool

def Lean.Name.isSuffixOf : Name → Name → Bool

def Lean.Name.cmp : Name → Name → Ordering

def Lean.Name.lt (x y : Name) : Bool

def Lean.Name.quickCmpAux : Name → Name → Ordering

def Lean.Name.quickCmp (n₁ n₂ : Name) : Ordering

def Lean.Name.quickLt (n₁ n₂ : Name) : Bool

def Lean.Name.hasNum : Name → Bool

Returns true if the name has any numeric components.

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).

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.

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.

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.

def Lean.Name.isAtomic : Name → Bool

def Lean.Name.isAnonymous : Name → Bool

def Lean.Name.isStr : Name → Bool

def Lean.Name.isNum : Name → Bool

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

def Lean.Name.isMetaprogramming (n : Name) : Bool

Return true if the name is in a namespace associated to metaprogramming.