def Lean.NameMap (α : Type) : Type

@[inline]

def Lean.mkNameMap (α : Type) : NameMap α

instance Lean.NameMap.instRepr {α : Type} [Repr α] : Repr (NameMap α)

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

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

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

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

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

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

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

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

def Lean.NameMap.filterMap {α β : Type} (f : Name → α → Option β) (m : NameMap α) : 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.

def Lean.NameSet : Type

def Lean.NameSet.empty : NameSet

instance Lean.NameSet.instEmptyCollection : EmptyCollection NameSet

instance Lean.NameSet.instInhabited : Inhabited NameSet

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

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

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

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

The union of two NameSets.

instance Lean.NameSet.instAppend : Append NameSet

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

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

def Lean.NameSSet : Type

@[reducible, inline]

abbrev Lean.NameSSet.empty : NameSSet

instance Lean.NameSSet.instEmptyCollection : EmptyCollection NameSSet

instance Lean.NameSSet.instInhabited : Inhabited NameSSet

@[reducible, inline]

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

@[reducible, inline]

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

def Lean.NameHashSet : Type

@[inline]

def Lean.NameHashSet.empty : NameHashSet

instance Lean.NameHashSet.instEmptyCollection : EmptyCollection NameHashSet

instance Lean.NameHashSet.instInhabited : Inhabited NameHashSet

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

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

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

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

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

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