source
def Lean.NameMap (α : Type) :
Type
Equations

- Lean.NameMap α = Std.TreeMap Lean.Name α Lean.Name.quickCmp

Instances For

source
@[inline]
def Lean.mkNameMap (α : Type) :
NameMap α
Equations

- Lean.mkNameMap α = Std.TreeMap.empty

Instances For

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

- Lean.NameMap.instRepr = inferInstanceAs (Repr (Std.TreeMap Lean.Name α Lean.Name.quickCmp))

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

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

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

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

source
def Lean.NameMap.insert {α : Type} (m : NameMap α) (n : Name) (a : α) :
Std.TreeMap Name α Name.quickCmp
Equations

- m.insert n a = Std.TreeMap.insert m n a

Instances For

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

- m.contains n = Std.TreeMap.contains m n

Instances For

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

- m.find? n = Std.TreeMap.get? m n

Instances For

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

- Lean.NameMap.instForInProdName = inferInstanceAs (ForIn m (Std.TreeMap Lean.Name α Lean.Name.quickCmp) (Lean.Name × α))

source
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`.

Equations

- Lean.NameMap.filter f m = Std.TreeMap.filter f m

Instances For

source
def Lean.NameSet :
Type
Equations

- Lean.NameSet = Std.TreeSet Lean.Name Lean.Name.quickCmp

Instances For

source
def Lean.NameSet.empty :
NameSet
Equations

- Lean.NameSet.empty = Std.TreeSet.empty

Instances For

source
instance Lean.NameSet.instEmptyCollection :
EmptyCollection NameSet
Equations

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

source
instance Lean.NameSet.instInhabited :
Inhabited NameSet
Equations

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

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

- s.insert n = Std.TreeSet.insert s n

Instances For

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

- s.contains n = Std.TreeSet.contains s n

Instances For

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

- Lean.NameSet.instForInName = inferInstanceAs (ForIn m (Std.TreeSet Lean.Name Lean.Name.quickCmp) Lean.Name)

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

The union of two `NameSet`s.

Equations

- s.append t = Std.TreeSet.merge s t

Instances For

source
instance Lean.NameSet.instAppend :
Append NameSet
Equations

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

source
instance Lean.NameSet.instSingletonName :
Singleton Name NameSet
Equations

- Lean.NameSet.instSingletonName = { singleton := fun (n : Lean.Name) => ∅.insert n }

source
instance Lean.NameSet.instUnion :
Union NameSet
Equations

- Lean.NameSet.instUnion = { union := Lean.NameSet.append }

source
instance Lean.NameSet.instInter :
Inter NameSet
Equations

- Lean.NameSet.instInter = { inter := fun (s t : Lean.NameSet) => Std.TreeSet.foldl (fun (r : Lean.NameSet) (n : Lean.Name) => if t.contains n = true then r.insert n else r) ∅ s }

source
instance Lean.NameSet.instSDiff :
SDiff NameSet
Equations

- Lean.NameSet.instSDiff = { sdiff := fun (s t : Lean.NameSet) => Std.TreeSet.foldl (fun (s : Lean.NameSet) (n : Lean.Name) => Std.TreeSet.erase s n) s t }

source
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`.

Equations

- Lean.NameSet.filter f s = Std.TreeSet.filter f s

Instances For

source
def Lean.NameSet.ofList (l : List Name) :
NameSet
Equations

- Lean.NameSet.ofList l = Std.TreeSet.ofList l Lean.Name.quickCmp

Instances For

source
def Lean.NameSet.ofArray (l : Array Name) :
NameSet
Equations

- Lean.NameSet.ofArray l = Std.TreeSet.ofArray l Lean.Name.quickCmp

Instances For

source
def Lean.NameSSet :
Type
Equations

- Lean.NameSSet = Lean.SSet Lean.Name

Instances For

source
@[reducible, inline]
abbrev Lean.NameSSet.empty :
NameSSet
Equations

- Lean.NameSSet.empty = Lean.SSet.empty

Instances For

source
instance Lean.NameSSet.instEmptyCollection :
EmptyCollection NameSSet
Equations

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

source
instance Lean.NameSSet.instInhabited :
Inhabited NameSSet
Equations

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

source
@[reducible, inline]
abbrev Lean.NameSSet.insert (s : NameSSet) (n : Name) :
NameSSet
Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.NameSSet.contains (s : NameSSet) (n : Name) :
Bool
Equations

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

Instances For

source
def Lean.NameHashSet :
Type
Equations

- Lean.NameHashSet = Std.HashSet Lean.Name

Instances For

source
@[inline]
def Lean.NameHashSet.empty :
NameHashSet
Equations

- Lean.NameHashSet.empty = ∅

Instances For

source
instance Lean.NameHashSet.instEmptyCollection :
EmptyCollection NameHashSet
Equations

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

source
instance Lean.NameHashSet.instInhabited :
Inhabited NameHashSet
Equations

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

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

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

Instances For

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

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

Instances For

source
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`.

Equations

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

Instances For

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

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

Instances For

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

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

Instances For