def Lean.NameMap (α : Type) : 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.instEmptyCollection (α : Type) : EmptyCollection (Lean.NameMap α)

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

instance Lean.NameMap.instForInProdName {α : Type} {m : Type u_1 → Type u_2} : ForIn m (Lean.NameMap α) (Lean.Name × α)

Equations

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

def Lean.NameMap.filter {α : Type} (f : Lean.Name → α → Bool) (m : Lean.NameMap α) : Lean.NameMap α

filter f m returns the NameMap consisting of all "key/val"-pairs in m where f key val returns true.

Equations

• Lean.NameMap.filter f m = Lean.RBMap.filter f m

def Lean.NameMap.filterMap {α β : Type} (f : Lean.Name → α → Option β) (m : Lean.NameMap α) : Lean.NameMap β

filterMap f m filters an NameMap and simultaneously modifies the filtered values.

It takes a function f : Name → α → Option β and applies f name to the value with key name. The resulting entries with non-none value are collected to form the output NameMap.

Equations

• Lean.NameMap.filterMap f m = Lean.RBMap.filterMap f m

def Lean.NameSet : Type

Equations

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

def Lean.NameSet.empty : Lean.NameSet

Equations

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

instance Lean.NameSet.instEmptyCollection : EmptyCollection Lean.NameSet

Equations

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

instance Lean.NameSet.instInhabited : Inhabited Lean.NameSet

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

The union of two NameSets.

Equations

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

instance Lean.NameSet.instAppend : Append Lean.NameSet

Equations

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

def Lean.NameSet.filter (f : Lean.Name → Bool) (s : Lean.NameSet) : Lean.NameSet

filter f s returns the NameSet consisting of all x in s where f x returns true.

Equations

• Lean.NameSet.filter f s = Lean.RBTree.filter f s

def Lean.NameSSet : Type

Equations

• Lean.NameSSet = Lean.SSet Lean.Name

@[reducible, inline]

abbrev Lean.NameSSet.empty : Lean.NameSSet

Equations

• Lean.NameSSet.empty = Lean.SSet.empty

instance Lean.NameSSet.instEmptyCollection : EmptyCollection Lean.NameSSet

Equations

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

instance Lean.NameSSet.instInhabited : Inhabited Lean.NameSSet

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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.instEmptyCollection : EmptyCollection Lean.NameHashSet

Equations

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

instance Lean.NameHashSet.instInhabited : Inhabited Lean.NameHashSet

Equations

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

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

Equations

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

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

Equations

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

def Lean.NameHashSet.filter (f : Lean.Name → Bool) (s : Lean.NameHashSet) : Lean.NameHashSet

filter f s returns the NameHashSet consisting of all x in s where f x returns true.

Equations

• Lean.NameHashSet.filter f s = Std.HashSet.filter f s

def Lean.MacroScopesView.isPrefixOf (v₁ 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)

def Lean.MacroScopesView.isSuffixOf (v₁ 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)