# Documentation

Lean.Data.SMap

structure Lean.SMap (α : Type u) (β : Type v) [inst : BEq α] [inst : ] :
Type (maxuv)
• stage₁ : Bool
• map₁ :
• map₂ :

Staged map for implementing the Environment. The idea is to store imported entries into a hashtable and local entries into a persistent hashtable.

Hypotheses:

• The number of entries (i.e., declarations) coming from imported files is much bigger than the number of entries in the current file.
• HashMap is faster than PersistentHashMap.

Remarks:

• We never remove declarations from the Environment. In principle, we could support deletion by using (PHashMap α (Option β)) where the value none would indicate that an entry was "removed" from the hashtable.
• We do not need additional bookkeeping for extracting the local entries.
Instances For
instance Lean.SMap.instInhabitedSMap {α : Type u} {β : Type v} [inst : BEq α] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
def Lean.SMap.empty {α : Type u} {β : Type v} [inst : BEq α] [inst : ] :
Equations
@[inline]
def Lean.SMap.fromHashMap {α : Type u} {β : Type v} [inst : BEq α] [inst : ] (m : ) (stage₁ : ) :
Equations
@[specialize #[]]
def Lean.SMap.insert {α : Type u} {β : Type v} [inst : BEq α] [inst : ] :
αβ
Equations
• One or more equations did not get rendered due to their size.
@[specialize #[]]
def Lean.SMap.insert' {α : Type u} {β : Type v} [inst : BEq α] [inst : ] :
αβ
Equations
• One or more equations did not get rendered due to their size.
@[specialize #[]]
def Lean.SMap.find? {α : Type u} {β : Type v} [inst : BEq α] [inst : ] :
α
Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.SMap.findD {α : Type u} {β : Type v} [inst : BEq α] [inst : ] (m : ) (a : α) (b₀ : β) :
β
Equations
@[inline]
def Lean.SMap.find! {α : Type u} {β : Type v} [inst : BEq α] [inst : ] [inst : ] (m : ) (a : α) :
β
Equations
@[specialize #[]]
def Lean.SMap.contains {α : Type u} {β : Type v} [inst : BEq α] [inst : ] :
αBool
Equations
• One or more equations did not get rendered due to their size.
@[specialize #[]]
def Lean.SMap.find?' {α : Type u} {β : Type v} [inst : BEq α] [inst : ] :
α

Similar to find?, but searches for result in the hashmap first. So, the result is correct only if we never "overwrite" map₁ entries using map₂.

Equations
• One or more equations did not get rendered due to their size.
def Lean.SMap.forM {α : Type u} {β : Type v} [inst : BEq α] [inst : ] {m : Type u_1 → Type u_1} [inst : ] (s : ) (f : αβ) :
Equations
def Lean.SMap.switch {α : Type u} {β : Type v} [inst : BEq α] [inst : ] (m : ) :

Move from stage 1 into stage 2.

Equations
• = if m.stage₁ = true then { stage₁ := false, map₁ := m.map₁, map₂ := m.map₂ } else m
@[inline]
def Lean.SMap.foldStage2 {α : Type u} {β : Type v} [inst : BEq α] [inst : ] {σ : Type w} (f : σαβσ) (s : σ) (m : ) :
σ
Equations
def Lean.SMap.fold {α : Type u} {β : Type v} [inst : BEq α] [inst : ] {σ : Type w} (f : σαβσ) (init : σ) (m : ) :
σ
Equations
def Lean.SMap.size {α : Type u} {β : Type v} [inst : BEq α] [inst : ] (m : ) :
Equations
def Lean.SMap.stageSizes {α : Type u} {β : Type v} [inst : BEq α] [inst : ] (m : ) :
Equations
def Lean.SMap.numBuckets {α : Type u} {β : Type v} [inst : BEq α] [inst : ] (m : ) :
Equations
def Lean.SMap.toList {α : Type u} {β : Type v} [inst : BEq α] [inst : ] (m : ) :
List (α × β)
Equations
def Lean.List.toSMap {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : ] (es : List (α × β)) :
Equations
• One or more equations did not get rendered due to their size.
instance Lean.instReprSMap {α : Type u_1} {β : Type u_2} :
{x : BEq α} → {x_1 : } → [inst : Repr α] → [inst : Repr β] → Repr ()
Equations