Documentation

Lean.Data.Name

instance Lean.instCoeStringName :

Coe String Lean.Name

Equations

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

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 s x => p | Lean.Name.num p s x => p

def Lean.Name.getString! :

Lean.Name → String

Equations

Lean.Name.getString! x = match x with | Lean.Name.str x s x_1 => s | x => panicWithPosWithDecl "Lean.Data.Name" "Lean.Name.getString!" 26 17 "unreachable code has been reached"

def Lean.Name.getNumParts :

Lean.Name → Nat

Equations

Lean.Name.getNumParts Lean.Name.anonymous = 0
Lean.Name.getNumParts (Lean.Name.str p s x_1) = Lean.Name.getNumParts p + 1
Lean.Name.getNumParts (Lean.Name.num p s x_1) = Lean.Name.getNumParts p + 1

def Lean.Name.updatePrefix :

Lean.Name → Lean.Name → Lean.Name

Equations

Lean.Name.updatePrefix x x = match x, x with | Lean.Name.anonymous, newP => Lean.Name.anonymous | Lean.Name.str p s x, newP => Lean.Name.mkStr newP s | Lean.Name.num p s x, newP => Lean.Name.mkNum newP s

def Lean.Name.components' :

Lean.Name → List Lean.Name

Equations

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

def Lean.Name.components (n : 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 x x = match x, x with | Lean.Name.str Lean.Name.anonymous s x, 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' x_2 x_3) = (x == Lean.Name.num p' x_2 x_3 || Lean.Name.isPrefixOf x p')
Lean.Name.isPrefixOf x (Lean.Name.str p' x_2 x_3) = (x == Lean.Name.str p' x_2 x_3 || 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₁ x_2) (Lean.Name.str p₂ s₂ x_3) = (s₁ == s₂ && Lean.Name.isSuffixOf p₁ p₂)
Lean.Name.isSuffixOf (Lean.Name.num p₁ n₁ x_2) (Lean.Name.num p₂ n₂ x_3) = (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₁ x_2) (Lean.Name.num p₂ i₂ x_3) = match Lean.Name.cmp p₁ p₂ with | Ordering.eq => compare i₁ i₂ | ord => ord
Lean.Name.cmp (Lean.Name.num x_2 x_3 x_4) (Lean.Name.str x_5 x_6 x_7) = Ordering.lt
Lean.Name.cmp (Lean.Name.str x_2 x_3 x_4) (Lean.Name.num x_5 x_6 x_7) = Ordering.gt
Lean.Name.cmp (Lean.Name.str p₁ n₁ x_2) (Lean.Name.str p₂ n₂ x_3) = match Lean.Name.cmp p₁ p₂ with | Ordering.eq => compare n₁ n₂ | ord => ord

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

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₁ x_2) (Lean.Name.num p₂ i₂ x_3) = match compare i₁ i₂ with | Ordering.eq => Lean.Name.quickCmpAux p₁ p₂ | ord => ord
Lean.Name.quickCmpAux (Lean.Name.num x_2 x_3 x_4) (Lean.Name.str x_5 x_6 x_7) = Ordering.lt
Lean.Name.quickCmpAux (Lean.Name.str x_2 x_3 x_4) (Lean.Name.num x_5 x_6 x_7) = Ordering.gt
Lean.Name.quickCmpAux (Lean.Name.str p₁ n₁ x_2) (Lean.Name.str p₂ n₂ x_3) = match compare n₁ n₂ with | Ordering.eq => Lean.Name.quickCmpAux p₁ p₂ | ord => ord

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

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) :

Equations

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

@[inline]

def Lean.Name.hasLtQuick :

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

Equations

Lean.Name.isInternal (Lean.Name.str p s x_1) = (String.get s 0 == Char.ofNat 95 || Lean.Name.isInternal p)
Lean.Name.isInternal (Lean.Name.num p x_1 x_2) = Lean.Name.isInternal p
Lean.Name.isInternal x = 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 x x_1 => true | Lean.Name.num Lean.Name.anonymous x x_1 => 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 x x_1 x_2 => true | x => false

def Lean.Name.isNum :

Lean.Name → Bool

Equations

Lean.Name.isNum x = match x with | Lean.Name.num x x_1 x_2 => true | x => false

noncomputable def Lean.NameMap (α : Type) :

Type

Equations

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

@[inline]

def Lean.mkNameMap (α : Type) :

Lean.NameMap α

Equations

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

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

EmptyCollection (Lean.NameMap α)

Equations

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

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

Inhabited (Lean.NameMap α)

Equations

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

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

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

Equations

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

@[inline]

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

Equations

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

noncomputable def Lean.NameSet :

Type

Equations

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

def Lean.NameSet.empty :

Equations

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

instance Lean.NameSet.instEmptyCollectionNameSet :

EmptyCollection Lean.NameSet

Equations

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

instance Lean.NameSet.instInhabitedNameSet :

Inhabited Lean.NameSet

Equations

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

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

Equations

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

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

Equations

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

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)

noncomputable def Lean.NameSSet :

Type

Equations

Lean.NameSSet = Lean.SSet Lean.Name

@[inline]

abbrev Lean.NameSSet.empty :

Equations

Lean.NameSSet.empty = Lean.SSet.empty

instance Lean.NameSSet.instEmptyCollectionNameSSet :

EmptyCollection Lean.NameSSet

Equations

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

instance Lean.NameSSet.instInhabitedNameSSet :

Inhabited Lean.NameSSet

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

noncomputable def Lean.NameHashSet :

Type

Equations

Lean.NameHashSet = Std.HashSet Lean.Name

@[inline]

def Lean.NameHashSet.empty :

Lean.NameHashSet

Equations

Lean.NameHashSet.empty = Std.HashSet.empty

instance Lean.NameHashSet.instEmptyCollectionNameHashSet :

EmptyCollection Lean.NameHashSet

Equations

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

instance Lean.NameHashSet.instInhabitedNameHashSet :

Inhabited Lean.NameHashSet

Equations

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

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

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

Equations

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

def String.toName (s : String) :

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