Documentation

Lean.Data.NameMap

instance Lean.instCoeStringName_1 :

Coe String Lean.Name

Equations

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

def Lean.NameMap (α : Type) :

Equations

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

@[inline]

def Lean.mkNameMap (α : Type) :

Lean.NameMap α

Equations

Lean.mkNameMap α = Lean.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 : α) :

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

Equations

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

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

Equations

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

@[inline]

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

Equations

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

instance Lean.NameMap.instForInNameMapProdName {α : Type} {m : Type u_1 → Type u_2} :

ForIn m (Lean.NameMap α) (Lean.Name × α)

Equations

Lean.NameMap.instForInNameMapProdName = inferInstanceAs (ForIn m (Lean.RBMap Lean.Name α Lean.Name.quickCmp) (Lean.Name × α))

def Lean.NameSet :

Equations

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

def Lean.NameSet.empty :

Equations

Lean.NameSet.empty = Lean.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 = Lean.RBTree.insert s n

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

Equations

Lean.NameSet.contains s n = Lean.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 (Lean.RBTree Lean.Name Lean.Name.quickCmp) Lean.Name)

def Lean.NameSSet :

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

def Lean.NameHashSet :

Equations

Lean.NameHashSet = Lean.HashSet Lean.Name

@[inline]

def Lean.NameHashSet.empty :

Lean.NameHashSet

Equations

Lean.NameHashSet.empty = Lean.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) :

Lean.HashSet Lean.Name

Equations

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

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

Equations

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

def Lean.MacroScopesView.isPrefixOf (v₁ : Lean.MacroScopesView) (v₂ : Lean.MacroScopesView) :

Equations

Lean.MacroScopesView.isPrefixOf v₁ v₂ = (Lean.Name.isPrefixOf v₁.name v₂.name && v₁.scopes == v₂.scopes && v₁.mainModule == v₂.mainModule && v₁.imported == v₂.imported)

def Lean.MacroScopesView.isSuffixOf (v₁ : Lean.MacroScopesView) (v₂ : Lean.MacroScopesView) :

Equations

Lean.MacroScopesView.isSuffixOf v₁ v₂ = (Lean.Name.isSuffixOf v₁.name v₂.name && v₁.scopes == v₂.scopes && v₁.mainModule == v₂.mainModule && v₁.imported == v₂.imported)