Lean.Data.Name

source

instance Lean.instCoeStringName:

Coe String Lean.Name

Equations

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

source

@[export lean_name_hash_exported]

def Lean.Name.hashEx:

Lean.Name → UInt64

Equations

Lean.Name.hashEx = Lean.Name.hash

source

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 a a_1 => p | Lean.Name.num p a a_1 => p

source

def Lean.Name.getString!:

Lean.Name → String

Equations

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

source

def Lean.Name.getNumParts:

Lean.Name → Nat

Equations

Lean.Name.getNumParts Lean.Name.anonymous = 0
Lean.Name.getNumParts (Lean.Name.str p a a_1) = Lean.Name.getNumParts p + 1
Lean.Name.getNumParts (Lean.Name.num p a a_1) = Lean.Name.getNumParts p + 1

source

def Lean.Name.updatePrefix:

Lean.Name → Lean.Name → Lean.Name

Equations

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

source

def Lean.Name.components':

Lean.Name → List Lean.Name

Equations

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

source

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

List Lean.Name

Equations

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

source

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 a, s' => s == s' | x, x_1 => false

source

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' a a_1) = (_fun_discr == Lean.Name.num p' a a_1 || Lean.Name.isPrefixOf _fun_discr p')
Lean.Name.isPrefixOf _fun_discr (Lean.Name.str p' a a_1) = (_fun_discr == Lean.Name.str p' a a_1 || Lean.Name.isPrefixOf _fun_discr p')

source

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₁ a) (Lean.Name.str p₂ s₂ a_1) = (s₁ == s₂ && Lean.Name.isSuffixOf p₁ p₂)
Lean.Name.isSuffixOf (Lean.Name.num p₁ n₁ a) (Lean.Name.num p₂ n₂ a_1) = (n₁ == n₂ && Lean.Name.isSuffixOf p₁ p₂)
Lean.Name.isSuffixOf _fun_discr _fun_discr = false

source

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₁ a) (Lean.Name.num p₂ i₂ a_1) = match Lean.Name.cmp p₁ p₂ with | Ordering.eq => compare i₁ i₂ | ord => ord
Lean.Name.cmp (Lean.Name.num a a_1 a_2) (Lean.Name.str a_3 a_4 a_5) = Ordering.lt
Lean.Name.cmp (Lean.Name.str a a_1 a_2) (Lean.Name.num a_3 a_4 a_5) = Ordering.gt
Lean.Name.cmp (Lean.Name.str p₁ n₁ a) (Lean.Name.str p₂ n₂ a_1) = match Lean.Name.cmp p₁ p₂ with | Ordering.eq => compare n₁ n₂ | ord => ord

source

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

Bool

Equations

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

source

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₁ a) (Lean.Name.num p₂ i₂ a_1) = match compare i₁ i₂ with | Ordering.eq => Lean.Name.quickCmpAux p₁ p₂ | ord => ord
Lean.Name.quickCmpAux (Lean.Name.num a a_1 a_2) (Lean.Name.str a_3 a_4 a_5) = Ordering.lt
Lean.Name.quickCmpAux (Lean.Name.str a a_1 a_2) (Lean.Name.num a_3 a_4 a_5) = Ordering.gt
Lean.Name.quickCmpAux (Lean.Name.str p₁ n₁ a) (Lean.Name.str p₂ n₂ a_1) = match compare n₁ n₂ with | Ordering.eq => Lean.Name.quickCmpAux p₁ p₂ | ord => ord

source

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

source

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

Bool

Equations

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

source

@[inline]

def Lean.Name.hasLtQuick:

LT Lean.Name

Equations

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

source

@[inline]

instance Lean.Name.instDecidableRelNameLtHasLtQuick:

DecidableRel LT.lt

Equations

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

source

def Lean.Name.isInternal:

Lean.Name → Bool

Equations

Lean.Name.isInternal (Lean.Name.str p s a) = (String.get s 0 == Char.ofNat 95 || Lean.Name.isInternal p)
Lean.Name.isInternal (Lean.Name.num p a a_1) = Lean.Name.isInternal p
Lean.Name.isInternal _fun_discr = false

source

def Lean.Name.isAtomic:

Lean.Name → Bool

Equations

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

source

def Lean.Name.isAnonymous:

Lean.Name → Bool

Equations

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

source

def Lean.Name.isStr:

Lean.Name → Bool

Equations

Lean.Name.isStr _fun_discr = match _fun_discr with | Lean.Name.str a a_1 a_2 => true | x => false

source

def Lean.Name.isNum:

Lean.Name → Bool

Equations

Lean.Name.isNum _fun_discr = match _fun_discr with | Lean.Name.num a a_1 a_2 => true | x => false

source

def Lean.NameMap (α : Type) :

Type

Equations

Lean.NameMap α = Std.RBMap Lean.Name α Lean.Name.quickCmp

source

@[inline]

def Lean.mkNameMap (α : Type) :

Lean.NameMap α

Equations

Lean.mkNameMap α = Std.mkRBMap Lean.Name α Lean.Name.quickCmp

source

instance Lean.NameMap.instEmptyCollectionNameMap (α : Type) :

EmptyCollection (Lean.NameMap α)

Equations

Lean.NameMap.instEmptyCollectionNameMap α = { emptyCollection := Lean.mkNameMap α }

source

instance Lean.NameMap.instInhabitedNameMap (α : Type) :

Inhabited (Lean.NameMap α)

Equations

Lean.NameMap.instInhabitedNameMap α = { default := ∅ }

source

def Lean.NameMap.insert {α : Type} (m : Lean.NameMap α) (n : Lean.Name) (a : α) :

Std.RBMap Lean.Name α Lean.Name.quickCmp

Equations

Lean.NameMap.insert m n a = Std.RBMap.insert m n a

source

def Lean.NameMap.contains {α : Type} (m : Lean.NameMap α) (n : Lean.Name) :

Bool

Equations

Lean.NameMap.contains m n = Std.RBMap.contains m n

source

@[inline]

def Lean.NameMap.find? {α : Type} (m : Lean.NameMap α) (n : Lean.Name) :

Option α

Equations

Lean.NameMap.find? m n = Std.RBMap.find? m n

source

def Lean.NameSet:

Type

Equations

Lean.NameSet = Std.RBTree Lean.Name Lean.Name.quickCmp

source

def Lean.NameSet.empty:

Lean.NameSet

Equations

Lean.NameSet.empty = Std.mkRBTree Lean.Name Lean.Name.quickCmp

source

instance Lean.NameSet.instEmptyCollectionNameSet:

EmptyCollection Lean.NameSet

Equations

Lean.NameSet.instEmptyCollectionNameSet = { emptyCollection := Lean.NameSet.empty }

source

instance Lean.NameSet.instInhabitedNameSet:

Inhabited Lean.NameSet

Equations

Lean.NameSet.instInhabitedNameSet = { default := Lean.NameSet.empty }

source

def Lean.NameSet.insert (s : Lean.NameSet) (n : Lean.Name) :

Lean.NameSet

Equations

Lean.NameSet.insert s n = Std.RBTree.insert s n

source

def Lean.NameSet.contains (s : Lean.NameSet) (n : Lean.Name) :

Bool

Equations

Lean.NameSet.contains s n = Std.RBMap.contains s n

source

instance Lean.NameSet.instForInNameSetName {m : Type u_1 → Type u_2} :

ForIn m Lean.NameSet Lean.Name

Equations

Lean.NameSet.instForInNameSetName = inferInstanceAs (ForIn m (Std.RBTree Lean.Name Lean.Name.quickCmp) Lean.Name)

source

def Lean.NameSSet:

Type

Equations

Lean.NameSSet = Lean.SSet Lean.Name

source

@[inline]

abbrev Lean.NameSSet.empty:

Lean.NameSSet

Equations

Lean.NameSSet.empty = Lean.SSet.empty

source

instance Lean.NameSSet.instEmptyCollectionNameSSet:

EmptyCollection Lean.NameSSet

Equations

Lean.NameSSet.instEmptyCollectionNameSSet = { emptyCollection := Lean.NameSSet.empty }

source

instance Lean.NameSSet.instInhabitedNameSSet:

Inhabited Lean.NameSSet

Equations

Lean.NameSSet.instInhabitedNameSSet = { default := Lean.NameSSet.empty }

source

@[inline]

abbrev Lean.NameSSet.insert (s : Lean.NameSSet) (n : Lean.Name) :

Lean.NameSSet

Equations

Lean.NameSSet.insert s n = Lean.SSet.insert s n

source

@[inline]

abbrev Lean.NameSSet.contains (s : Lean.NameSSet) (n : Lean.Name) :

Bool

Equations

Lean.NameSSet.contains s n = Lean.SSet.contains s n

source

def Lean.NameHashSet:

Type

Equations

Lean.NameHashSet = Std.HashSet Lean.Name

source

@[inline]

def Lean.NameHashSet.empty:

Lean.NameHashSet

Equations

Lean.NameHashSet.empty = Std.HashSet.empty

source

instance Lean.NameHashSet.instEmptyCollectionNameHashSet:

EmptyCollection Lean.NameHashSet

Equations

Lean.NameHashSet.instEmptyCollectionNameHashSet = { emptyCollection := Lean.NameHashSet.empty }

source

instance Lean.NameHashSet.instInhabitedNameHashSet:

Inhabited Lean.NameHashSet

Equations

Lean.NameHashSet.instInhabitedNameHashSet = { default := ∅ }

source

def Lean.NameHashSet.insert (s : Lean.NameHashSet) (n : Lean.Name) :

Std.HashSet Lean.Name

Equations

Lean.NameHashSet.insert s n = Std.HashSet.insert s n

source

def Lean.NameHashSet.contains (s : Lean.NameHashSet) (n : Lean.Name) :

Bool

Equations

Lean.NameHashSet.contains s n = Std.HashSet.contains s n

source

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