instance Lean.instCoeStringName : Coe String Lean.Name

Equations

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

@[export lean_name_hash_exported]

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

Equations

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

def Lean.Name.getPrefix : Lean.Name → Lean.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! : Lean.Name → String

Equations

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

def Lean.Name.getNumParts : Lean.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 : Lean.Name → Lean.Name → Lean.Name

Equations

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

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

Equations

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

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

Equations

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

def Lean.Name.quickCmpAux : Lean.Name → Lean.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

def Lean.Name.quickCmp (n₁ : Lean.Name) (n₂ : Lean.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

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

Equations

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

@[inline]

def Lean.Name.hasLtQuick : LT Lean.Name

Alternative HasLt instance.

Equations

• Lean.Name.hasLtQuick = { lt := fun a b => Lean.Name.quickLt a b = true }

@[inline]

def Lean.Name.Name.decLt : DecidableRel LT.lt

Equations

• Lean.Name.Name.decLt = inferInstanceAs (DecidableRel fun a b => Lean.Name.quickLt a b = true)

instance Lean.Name.instDecidableRelNameLtHasLtQuick : DecidableRel LT.lt

Equations

• Lean.Name.instDecidableRelNameLtHasLtQuick = Lean.Name.Name.decLt

def Lean.Name.isInternal : Lean.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 == Char.ofNat 95 || Lean.Name.isInternal p)
• Lean.Name.isInternal (Lean.Name.num p i) = Lean.Name.isInternal p
• Lean.Name.isInternal x = false

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

Equations

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

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

Equations

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

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

Equations

• Lean.Name.isNum x = match x with | Lean.Name.num pre i => true | x => false

def Lean.Name.anyS (n : Lean.Name) (f : String → Bool) : Bool

Return true if n contains a string part s that satifies 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

def String.toName (s : String) : Lean.Name

Equations

• String.toName s = let ps := String.splitOn s "."; List.foldl (fun n p => Lean.Name.mkStr n (String.trim p)) Lean.Name.anonymous ps