Lean.Data.NameMap

source

def Lean.NameMap (α : Type) :

Type

Equations

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

Instances For

source

@[inline]

def Lean.mkNameMap (α : Type) :

Lake.NameMap α

Equations

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

source

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

EmptyCollection (Lake.NameMap α)

Equations

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

source

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

Inhabited (Lake.NameMap α)

Equations

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

source

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

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

Equations

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

source

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

Bool

Equations

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

source

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

Option α

Equations

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

source

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

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

Equations

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

source

def Lean.NameSet :

Type

Equations

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

Instances For

source

def Lean.NameSet.empty :

Lean.NameSet

Equations

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

source

instance Lean.NameSet.instEmptyCollection :

EmptyCollection Lean.NameSet

Equations

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

source

instance Lean.NameSet.instInhabited :

Inhabited Lean.NameSet

Equations

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

source

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

Lean.NameSet

Equations

s.insert n = Lean.RBTree.insert s n

source

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

Bool

Equations

s.contains n = Lean.RBMap.contains s n

source

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

ForIn m Lean.NameSet Lake.Name

Equations

Lean.NameSet.instForInName = inferInstanceAs (ForIn m (Lean.RBTree Lake.Name Lean.Name.quickCmp) Lake.Name)

source

def Lean.NameSet.append (s : Lean.NameSet) (t : Lean.NameSet) :

Lean.NameSet

The union of two NameSets.

Equations

s.append t = Lean.RBMap.mergeBy (fun (x : Lake.Name) (x x : Unit) => ()) s t

source

instance Lean.NameSet.instAppend :

Append Lean.NameSet

Equations

Lean.NameSet.instAppend = { append := Lean.NameSet.append }

source

def Lean.NameSSet :

Type

Equations

Lean.NameSSet = Lean.SSet Lake.Name

Instances For

source

@[reducible, inline]

abbrev Lean.NameSSet.empty :

Lean.NameSSet

Equations

Lean.NameSSet.empty = Lean.SSet.empty

source

instance Lean.NameSSet.instEmptyCollection :

EmptyCollection Lean.NameSSet

Equations

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

source

instance Lean.NameSSet.instInhabited :

Inhabited Lean.NameSSet

Equations

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

source

@[reducible, inline]

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

Lean.NameSSet

Equations

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

source

@[reducible, inline]

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

Bool

Equations

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

source

def Lean.NameHashSet :

Type

Equations

Lean.NameHashSet = Std.HashSet Lake.Name

Instances For

source

@[inline]

def Lean.NameHashSet.empty :

Lean.NameHashSet

Equations

Lean.NameHashSet.empty = Std.HashSet.empty

source

instance Lean.NameHashSet.instEmptyCollection :

EmptyCollection Lean.NameHashSet

Equations

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

source

instance Lean.NameHashSet.instInhabited :

Inhabited Lean.NameHashSet

Equations

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

source

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

Std.HashSet Lake.Name

Equations

s.insert n = Std.HashSet.insert s n

source

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

Bool

Equations

s.contains n = Std.HashSet.contains s n

source

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

Bool

Equations

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

source

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

Bool

Equations

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