structure Lean.SMap (α : Type u) (β : Type v) [BEq α] [Hashable α] : Type (max u v)

• stage₁ : Bool
• map₁ : Lean.HashMap α β
• map₂ : Lean.PHashMap α β

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.
• When we are reading imported files, we have exclusive access to the map, and efficient destructive updates are performed.

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.

instance Lean.SMap.instInhabitedSMap {α : Type u} {β : Type v} [BEq α] [Hashable α] : Inhabited (Lean.SMap α β)

def Lean.SMap.empty {α : Type u} {β : Type v} [BEq α] [Hashable α] : Lean.SMap α β

@[inline]

def Lean.SMap.fromHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.HashMap α β) (stage₁ : optParam Bool true) : Lean.SMap α β

@[specialize #[]]

def Lean.SMap.insert {α : Type u} {β : Type v} [BEq α] [Hashable α] : Lean.SMap α β → α → β → Lean.SMap α β

@[specialize #[]]

def Lean.SMap.insert' {α : Type u} {β : Type v} [BEq α] [Hashable α] : Lean.SMap α β → α → β → Lean.SMap α β

@[specialize #[]]

def Lean.SMap.find? {α : Type u} {β : Type v} [BEq α] [Hashable α] : Lean.SMap α β → α → Option β

@[inline]

def Lean.SMap.findD {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.SMap α β) (a : α) (b₀ : β) : β

@[inline]

def Lean.SMap.find! {α : Type u} {β : Type v} [BEq α] [Hashable α] [Inhabited β] (m : Lean.SMap α β) (a : α) : β

@[specialize #[]]

def Lean.SMap.contains {α : Type u} {β : Type v} [BEq α] [Hashable α] : Lean.SMap α β → α → Bool

@[specialize #[]]

def Lean.SMap.find?' {α : Type u} {β : Type v} [BEq α] [Hashable α] : Lean.SMap α β → α → Option β

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₂.

def Lean.SMap.forM {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Type u_1 → Type u_1} [Monad m] (s : Lean.SMap α β) (f : α → β → m PUnit) : m PUnit

def Lean.SMap.switch {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.SMap α β) : Lean.SMap α β

Move from stage 1 into stage 2.

@[inline]

def Lean.SMap.foldStage2 {α : Type u} {β : Type v} [BEq α] [Hashable α] {σ : Type w} (f : σ → α → β → σ) (s : σ) (m : Lean.SMap α β) : σ

def Lean.SMap.fold {α : Type u} {β : Type v} [BEq α] [Hashable α] {σ : Type w} (f : σ → α → β → σ) (init : σ) (m : Lean.SMap α β) : σ

def Lean.SMap.size {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.SMap α β) : Nat

def Lean.SMap.stageSizes {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.SMap α β) : Nat × Nat

def Lean.SMap.numBuckets {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.SMap α β) : Nat

def Lean.SMap.toList {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.SMap α β) : List (α × β)

def Lean.List.toSMap {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (es : List (α × β)) : Lean.SMap α β

instance Lean.instReprSMap {α : Type u_1} {β : Type u_2} : {x : BEq α} → {x_1 : Hashable α} → [inst : Repr α] → [inst : Repr β] → Repr (Lean.SMap α β)