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 _fun_discr = match _fun_discr 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.components' : Lean.Name → List Lean.Name

Equations

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

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

Equations

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

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

Equations

• Lean.Name.eqStr _fun_discr _fun_discr = match _fun_discr, _fun_discr 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 _fun_discr Lean.Name.anonymous = (_fun_discr == Lean.Name.anonymous)
• Lean.Name.isPrefixOf _fun_discr (Lean.Name.num p' i) = (_fun_discr == Lean.Name.num p' i || Lean.Name.isPrefixOf _fun_discr p')
• Lean.Name.isPrefixOf _fun_discr (Lean.Name.str p' str) = (_fun_discr == Lean.Name.str p' str || Lean.Name.isPrefixOf _fun_discr p')

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

Equations

• Lean.Name.isSuffixOf Lean.Name.anonymous _fun_discr = 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 _fun_discr _fun_discr = 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 _fun_discr = Ordering.lt
• Lean.Name.cmp _fun_discr 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 _fun_discr = Ordering.lt
• Lean.Name.quickCmpAux _fun_discr 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]

instance Lean.Name.instDecidableRelNameLtHasLtQuick : DecidableRel LT.lt

Equations

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

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 _fun_discr = false

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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