@[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

• x.getPrefix = match x with | Lean.Name.anonymous => Lean.Name.anonymous | p.str str => p | p.num i => p

def Lean.Name.getString! : Lake.Name → String

Equations

• x.getString! = match x with | pre.str s => s | x => 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

• x✝.updatePrefix x = match x✝, x with | Lean.Name.anonymous, x => Lean.Name.anonymous | pre.str s, newP => newP.mkStr s | pre.num s, newP => newP.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

• x✝.eqStr x = match x✝, x with | Lean.Name.anonymous.str s, s' => s == s' | x, x_1 => 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.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

• x.isAtomic = match x with | Lean.Name.anonymous => true | Lean.Name.anonymous.str str => true | Lean.Name.anonymous.num i => true | x => false

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

Equations

• x.isAnonymous = match x with | Lean.Name.anonymous => true | x => false

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

Equations

• x.isStr = match x with | pre.str str => true | x => false

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

Equations

• x.isNum = match x with | pre.num i => true | x => 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