instance Lean.instCoeStringName_1 : Coe String Lake.Name

def Lean.NameMap (α : Type) : Type

@[inline]

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

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

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

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

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

@[inline]

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

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

def Lean.NameSet : Type

def Lean.NameSet.empty : Lean.NameSet

instance Lean.NameSet.instEmptyCollectionNameSet : EmptyCollection Lean.NameSet

instance Lean.NameSet.instInhabitedNameSet : Inhabited Lean.NameSet

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

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

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

def Lean.NameSSet : Type

@[inline, reducible]

abbrev Lean.NameSSet.empty : Lean.NameSSet

instance Lean.NameSSet.instEmptyCollectionNameSSet : EmptyCollection Lean.NameSSet

instance Lean.NameSSet.instInhabitedNameSSet : Inhabited Lean.NameSSet

@[inline, reducible]

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

@[inline, reducible]

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

def Lean.NameHashSet : Type

@[inline]

def Lean.NameHashSet.empty : Lean.NameHashSet

instance Lean.NameHashSet.instEmptyCollectionNameHashSet : EmptyCollection Lean.NameHashSet

instance Lean.NameHashSet.instInhabitedNameHashSet : Inhabited Lean.NameHashSet

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

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

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

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