Documentation

Lean.Data.HashMap

def Lean.HashMapBucket (α : Type u) (β : Type v) :
Type (max 0 u v)
Equations
def Lean.HashMapBucket.update {α : Type u} {β : Type v} (data : HashMapBucket α β) (i : USize) (d : AssocList α β) (h : i.toNat < data.val.size) :
Equations
@[simp]
theorem Lean.HashMapBucket.size_update {α : Type u} {β : Type v} (data : HashMapBucket α β) (i : USize) (d : AssocList α β) (h : i.toNat < data.val.size) :
(data.update i d h).val.size = data.val.size
@[deprecated Std.HashMap.Raw (since := "2024-08-08")]
structure Lean.HashMapImp (α : Type u) (β : Type v) :
Type (max u v)
@[deprecated Std.HashMap.Raw.empty (since := "2024-08-08")]
def Lean.mkHashMapImp {α : Type u} {β : Type v} (capacity : Nat := 8) :
Equations
@[inline]
def Lean.HashMapImp.reinsertAux {α : Type u} {β : Type v} (hashFn : αUInt64) (data : HashMapBucket α β) (a : α) (b : β) :
Equations
@[inline]
def Lean.HashMapImp.foldBucketsM {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashMapBucket α β) (d : δ) (f : δαβm δ) :
m δ
Equations
@[inline]
def Lean.HashMapImp.foldBuckets {α : Type u} {β : Type v} {δ : Type w} (data : HashMapBucket α β) (d : δ) (f : δαβδ) :
δ
Equations
@[inline]
def Lean.HashMapImp.foldM {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Monad m] (f : δαβm δ) (d : δ) (h : HashMapImp α β) :
m δ
Equations
@[inline]
def Lean.HashMapImp.fold {α : Type u} {β : Type v} {δ : Type w} (f : δαβδ) (d : δ) (m : HashMapImp α β) :
δ
Equations
@[inline]
def Lean.HashMapImp.forBucketsM {α : Type u} {β : Type v} {m : Type w → Type w} [Monad m] (data : HashMapBucket α β) (f : αβm PUnit) :
Equations
@[inline]
def Lean.HashMapImp.forM {α : Type u} {β : Type v} {m : Type w → Type w} [Monad m] (f : αβm PUnit) (h : HashMapImp α β) :
Equations
def Lean.HashMapImp.findEntry? {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) :
Option (α × β)
Equations
def Lean.HashMapImp.find? {α : Type u} {β : Type v} [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) :
Equations
def Lean.HashMapImp.contains {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) :
Equations
@[irreducible]
def Lean.HashMapImp.moveEntries {α : Type u} {β : Type v} [Hashable α] (i : Nat) (source : Array (AssocList α β)) (target : HashMapBucket α β) :
Equations
  • One or more equations did not get rendered due to their size.
def Lean.HashMapImp.expand {α : Type u} {β : Type v} [Hashable α] (size : Nat) (buckets : HashMapBucket α β) :
Equations
@[inline]
def Lean.HashMapImp.insert {α : Type u} {β : Type v} [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) :
Equations
  • One or more equations did not get rendered due to their size.
@[inline]
def Lean.HashMapImp.insertIfNew {α : Type u} {β : Type v} [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) :
Equations
  • One or more equations did not get rendered due to their size.
def Lean.HashMapImp.erase {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) :
Equations
  • One or more equations did not get rendered due to their size.
inductive Lean.HashMapImp.WellFormed {α : Type u} {β : Type v} [BEq α] [Hashable α] :
HashMapImp α βProp
@[deprecated Std.HashMap (since := "2024-08-08")]
def Lean.HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :
Type (max 0 u v)
Equations
Instances For
@[deprecated Std.HashMap.empty (since := "2024-08-08")]
def Lean.mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (capacity : Nat := 8) :
HashMap α β
Equations
instance Lean.HashMap.instInhabited {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] :
Equations
instance Lean.HashMap.instEmptyCollection {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] :
Equations
@[inline, deprecated Std.HashMap.empty (since := "2024-08-08")]
def Lean.HashMap.empty {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] :
HashMap α β
Equations
@[deprecated Std.HashMap.insert (since := "2024-08-08")]
def Lean.HashMap.insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : HashMap α β) (a : α) (b : β) :
HashMap α β
Equations
@[deprecated Std.HashMap.containsThenInsert (since := "2024-08-08")]
def Lean.HashMap.insert' {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : HashMap α β) (a : α) (b : β) :

Similar to insert, but also returns a Boolean flag indicating whether an existing entry has been replaced with a -> b.

Equations
@[deprecated Std.HashMap.insertIfNew (since := "2024-08-08")]
def Lean.HashMap.insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : HashMap α β) (a : α) (b : β) :
HashMap α β × Option β

Similar to insert, but returns some old if the map already had an entry α → old. If the result is some old, the resulting map is equal to m.

Equations
@[inline, deprecated Std.HashMap.erase (since := "2024-08-08")]
def Lean.HashMap.erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : HashMap α β) (a : α) :
HashMap α β
Equations
@[inline, deprecated "Use `m[k]?` instead." (since := "2024-08-08")]
def Lean.HashMap.findEntry? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : HashMap α β) (a : α) :
Option (α × β)
Equations
@[inline, deprecated "Use `m[k]?` instead." (since := "2024-08-08")]
def Lean.HashMap.find? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : HashMap α β) (a : α) :
Equations
@[inline, deprecated "Use `m[k]?.getD` instead." (since := "2024-08-08")]
def Lean.HashMap.findD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : HashMap α β) (a : α) (b₀ : β) :
β
Equations
@[inline, deprecated "Use `m[k]!` instead." (since := "2024-08-08")]
def Lean.HashMap.find! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [Inhabited β] (m : HashMap α β) (a : α) :
β
Equations
instance Lean.HashMap.instGetElemOptionTrue {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} :
GetElem (HashMap α β) α (Option β) fun (x : HashMap α β) (x : α) => True
Equations
@[inline, deprecated Std.HashMap.contains (since := "2024-08-08")]
def Lean.HashMap.contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : HashMap α β) (a : α) :
Equations
@[inline, deprecated Std.HashMap.foldM (since := "2024-08-08")]
def Lean.HashMap.foldM {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {δ : Type w} {m : Type w → Type w} [Monad m] (f : δαβm δ) (init : δ) (h : HashMap α β) :
m δ
Equations
@[inline, deprecated Std.HashMap.fold (since := "2024-08-08")]
def Lean.HashMap.fold {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {δ : Type w} (f : δαβδ) (init : δ) (m : HashMap α β) :
δ
Equations
@[inline, deprecated Std.HashMap.forM (since := "2024-08-08")]
def Lean.HashMap.forM {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Type w → Type w} [Monad m] (f : αβm PUnit) (h : HashMap α β) :
Equations
@[inline, deprecated Std.HashMap.size (since := "2024-08-08")]
def Lean.HashMap.size {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : HashMap α β) :
Equations
@[inline, deprecated Std.HashMap.isEmpty (since := "2024-08-08")]
def Lean.HashMap.isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : HashMap α β) :
Equations
@[deprecated Std.HashMap.toList (since := "2024-08-08")]
def Lean.HashMap.toList {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : HashMap α β) :
List (α × β)
Equations
@[deprecated Std.HashMap.toArray (since := "2024-08-08")]
def Lean.HashMap.toArray {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : HashMap α β) :
Array (α × β)
Equations
@[deprecated "Deprecateed without a replacement." (since := "2024-08-08")]
def Lean.HashMap.numBuckets {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : HashMap α β) :
Equations
@[deprecated Std.HashMap.ofList (since := "2024-08-08")]
def Lean.HashMap.ofList {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) :
HashMap α β

Builds a HashMap from a list of key-value pairs. Values of duplicated keys are replaced by their respective last occurrences.

Equations
@[deprecated "Deprecateed without a replacement." (since := "2024-08-08")]
def Lean.HashMap.ofListWith {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) (f : βββ) :
HashMap α β

Variant of ofList which accepts a function that combines values of duplicated keys.

Equations
  • One or more equations did not get rendered due to their size.