@[export lean_name_hash_exported]

def Lean.Name.hashEx : Name → UInt64

Equations

• Lean.Name.hashEx = Lean.Name.hash

def Lean.Name.getPrefix : Name → Name

Equations

• Lean.Name.anonymous.getPrefix = Lean.Name.anonymous
• (p.str str).getPrefix = p
• (p.num i).getPrefix = p

def Lean.Name.getString! : Name → String

Equations

• (pre.str s).getString! = s
• x✝.getString! = panicWithPosWithDecl "Lean.Data.Name" "Lean.Name.getString!" 22 15 "unreachable code has been reached"

def Lean.Name.getNumParts : Name → Nat

Equations

• Lean.Name.anonymous.getNumParts = 0
• (p.str str).getNumParts = p.getNumParts + 1
• (p.num i).getNumParts = p.getNumParts + 1

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

Equations

• Lean.Name.anonymous.updatePrefix x✝ = Lean.Name.anonymous
• (pre.str s).updatePrefix x✝ = x✝.mkStr s
• (pre.num s).updatePrefix x✝ = x✝.mkNum s

def Lean.Name.componentsRev : Name → List Name

Equations

• Lean.Name.anonymous.componentsRev = []
• (p.str str).componentsRev = Lean.Name.anonymous.mkStr str :: p.componentsRev
• (p.num i).componentsRev = Lean.Name.anonymous.mkNum i :: p.componentsRev

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

Equations

• n.components = n.componentsRev.reverse

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

Equations

• (Lean.Name.anonymous.str s).eqStr x✝ = (s == x✝)
• x✝¹.eqStr x✝ = false

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

Equations

• x✝.isPrefixOf Lean.Name.anonymous = (x✝ == Lean.Name.anonymous)
• x✝.isPrefixOf (p'.num i) = (x✝ == p'.num i || x✝.isPrefixOf p')
• x✝.isPrefixOf (p'.str str) = (x✝ == p'.str str || x✝.isPrefixOf p')

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

Equations

• Lean.Name.anonymous.isSuffixOf x✝ = true
• (p₁.str s₁).isSuffixOf (p₂.str s₂) = (s₁ == s₂ && p₁.isSuffixOf p₂)
• (p₁.num n₁).isSuffixOf (p₂.num n₂) = (n₁ == n₂ && p₁.isSuffixOf p₂)
• x✝¹.isSuffixOf x✝ = false

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

Equations

• Lean.Name.anonymous.cmp Lean.Name.anonymous = Ordering.eq
• Lean.Name.anonymous.cmp x✝ = Ordering.lt
• x✝.cmp Lean.Name.anonymous = Ordering.gt
• (p₁.num i₁).cmp (p₂.num i₂) = match p₁.cmp p₂ with | Ordering.eq => compare i₁ i₂ | ord => ord
• (pre.num i).cmp (pre_1.str str) = Ordering.lt
• (pre.str str).cmp (pre_1.num i) = Ordering.gt
• (p₁.str n₁).cmp (p₂.str n₂) = match p₁.cmp p₂ with | Ordering.eq => compare n₁ n₂ | ord => ord

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

Equations

• x.lt y = (x.cmp y == Ordering.lt)

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

Equations

• Lean.Name.anonymous.quickCmpAux Lean.Name.anonymous = Ordering.eq
• Lean.Name.anonymous.quickCmpAux x✝ = Ordering.lt
• x✝.quickCmpAux Lean.Name.anonymous = Ordering.gt
• (p₁.num i₁).quickCmpAux (p₂.num i₂) = match compare i₁ i₂ with | Ordering.eq => p₁.quickCmpAux p₂ | ord => ord
• (pre.num i).quickCmpAux (pre_1.str str) = Ordering.lt
• (pre.str str).quickCmpAux (pre_1.num i) = Ordering.gt
• (p₁.str n₁).quickCmpAux (p₂.str n₂) = match compare n₁ n₂ with | Ordering.eq => p₁.quickCmpAux p₂ | ord => ord

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

Equations

• n₁.quickCmp n₂ = match compare n₁.hash n₂.hash with | Ordering.eq => n₁.quickCmpAux n₂ | ord => ord

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

Equations

• n₁.quickLt n₂ = (n₁.quickCmp n₂ == Ordering.lt)

def Lean.Name.hasNum : Name → Bool

Returns true if the name has any numeric components.

Equations

• Lean.Name.anonymous.hasNum = false
• (p.str str).hasNum = p.hasNum
• (p.num i).hasNum = true

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

• (p.str s).isInternal = (s.get 0 == '_' || p.isInternal)
• (p.num i).isInternal = p.isInternal
• x✝.isInternal = false

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

• (p.str s).isInternalOrNum = (s.get 0 == '_' || p.isInternalOrNum)
• (p.num i).isInternalOrNum = true
• x✝.isInternalOrNum = false

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

• One or more equations did not get rendered due to their size.
• (p.num i).isInternalDetail = true
• x✝.isInternalDetail = x✝.isInternalOrNum

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

Check that a string begins with the given prefix, and then is only digits/'_'.

Equations

• Lean.Name.isInternalDetail.matchPrefix s pre = (s.startsWith pre && (s.drop pre.length).all fun (c : Char) => c.isDigit || c == '_')

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

• (Lean.Name.anonymous.str s).isImplementationDetail = s.startsWith "__"
• (p.num i).isImplementationDetail = p.isImplementationDetail
• (p.str str).isImplementationDetail = p.isImplementationDetail
• Lean.Name.anonymous.isImplementationDetail = false

def Lean.Name.isAtomic : Name → Bool

Equations

• Lean.Name.anonymous.isAtomic = true
• (Lean.Name.anonymous.str str).isAtomic = true
• (Lean.Name.anonymous.num i).isAtomic = true
• x✝.isAtomic = false

def Lean.Name.isAnonymous : Name → Bool

Equations

• Lean.Name.anonymous.isAnonymous = true
• x✝.isAnonymous = false

def Lean.Name.isStr : Name → Bool

Equations

• (pre.str s).isStr = true
• x✝.isStr = false

def Lean.Name.isNum : Name → Bool

Equations

• (pre.num i).isNum = true
• x✝.isNum = false

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

• (p.str s).anyS f = (f s || p.anyS f)
• (p.num i).anyS f = p.anyS f
• n.anyS f = false