instance Lean.instCoeStringName : Coe String Lake.Name

Equations

• Lean.instCoeStringName = { coe := Lean.Name.mkSimple }

@[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.getPrefix x = match x with | Lean.Name.anonymous => Lean.Name.anonymous | Lean.Name.str p str => p | Lean.Name.num p i => p

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Name.getNumParts : Lake.Name → Nat

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Name.componentsRev : Lake.Name → List Lake.Name

Equations

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

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

Equations

• Lean.Name.components n = List.reverse (Lean.Name.componentsRev n)

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

Equations

• Lean.Name.eqStr x✝ x = match x✝, x with | Lean.Name.str Lean.Name.anonymous s, s' => s == s' | x, x_1 => false

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

Instances For

• Lake.Name.instLawfulCmpEqNameQuickCmpAux

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

Equations

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

Instances For

• Lake.Name.instLawfulCmpEqNameQuickCmp

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

Equations

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

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

Returns true if the name has any numeric components.

Equations

• Lean.Name.hasNum Lean.Name.anonymous = false
• Lean.Name.hasNum (Lean.Name.str p str) = Lean.Name.hasNum p
• Lean.Name.hasNum (Lean.Name.num p i) = 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

• Lean.Name.isInternal (Lean.Name.str p s) = (String.get s 0 == '_' || Lean.Name.isInternal p)
• Lean.Name.isInternal (Lean.Name.num p i) = Lean.Name.isInternal p
• Lean.Name.isInternal x = 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

• Lean.Name.isInternalOrNum (Lean.Name.str p s) = (String.get s 0 == '_' || Lean.Name.isInternalOrNum p)
• Lean.Name.isInternalOrNum (Lean.Name.num p i) = true
• Lean.Name.isInternalOrNum x = 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.isImplementationDetail (Lean.Name.str Lean.Name.anonymous s) = String.startsWith s "__"
• Lean.Name.isImplementationDetail (Lean.Name.num p i) = Lean.Name.isImplementationDetail p
• Lean.Name.isImplementationDetail (Lean.Name.str p str) = Lean.Name.isImplementationDetail p
• Lean.Name.isImplementationDetail Lean.Name.anonymous = false

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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