instance Lean.instCoeStringName_1 : Coe String Lake.Name

Equations

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

def Lean.NameMap (α : Type) : Type

Equations

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

@[inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

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 (Lake.NameMap α) (Lake.Name × α)

Equations

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

def Lean.NameSet : Type

Equations

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

def Lean.NameSet.empty : Lean.NameSet

Equations

• Lean.NameSet.empty = Lean.mkRBTree Lake.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 : Lake.Name) : Lean.NameSet

Equations

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

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

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 Lake.Name

Equations

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

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

The union of two NameSets.

Equations

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

instance Lean.NameSet.instAppendNameSet : Append Lean.NameSet

Equations

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

def Lean.NameSSet : Type

Equations

• Lean.NameSSet = Lean.SSet Lake.Name

@[inline, reducible]

abbrev Lean.NameSSet.empty : Lean.NameSSet

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, reducible]

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

Equations

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

@[inline, reducible]

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

Equations

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

def Lean.NameHashSet : Type

Equations

• Lean.NameHashSet = Lean.HashSet Lake.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 : Lake.Name) : Lean.HashSet Lake.Name

Equations

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

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

Equations

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

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

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) : Bool

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)