@[export lean_name_hash_exported]

def Lean.Name.hashEx : Lake.Name → UInt64

Equations

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

def Lean.Name.getPrefix : Lake.Name → Lake.Name

Equations

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

def Lean.Name.getString! : Lake.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 : Lake.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 : Lake.Name → Lake.Name → Lake.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 : Lake.Name → List Lake.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 : Lake.Name) : List Lake.Name

Equations

• n.components = n.componentsRev.reverse

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

Equations

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

def Lean.Name.isPrefixOf : Lake.Name → Lake.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 : Lake.Name → Lake.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 : Lake.Name → Lake.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 : Lake.Name) (y : Lake.Name) : Bool

Equations

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

def Lean.Name.quickCmpAux : Lake.Name → Lake.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₁ : Lake.Name) (n₂ : Lake.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₁ : Lake.Name) (n₂ : Lake.Name) : Bool

Equations

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

def Lean.Name.hasNum : Lake.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 : Lake.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 : Lake.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 : Lake.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 : String) (pre : String) : Bool

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

Equations

• Lean.Name.isInternalDetail.matchPrefix s pre = (s.startsWith pre && (s.drop pre.length).all Char.isDigit)

def Lean.Name.isImplementationDetail : Lake.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 : Lake.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 : Lake.Name → Bool

Equations

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

def Lean.Name.isStr : Lake.Name → Bool

Equations

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

def Lean.Name.isNum : Lake.Name → Bool

Equations

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

def Lean.Name.anyS (n : Lake.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