Documentation

Std.Data.HashMap

noncomputable def Std.HashMapBucket (α : Type u) (β : Type v) :
Type (max 0 u v)
Equations
def Std.HashMapBucket.update {α : Type u} {β : Type v} (data : Std.HashMapBucket α β) (i : USize) (d : Std.AssocList α β) (h : USize.toNat i < Array.size data.val) :
Equations
structure Std.HashMapImp (α : Type u) (β : Type v) :
Type (max u v)
def Std.mkHashMapImp {α : Type u} {β : Type v} (capacity : optParam Nat 0) :
Equations
def Std.HashMapImp.mkIdx {n : Nat} (h : n > 0) (u : USize) :
{ u // USize.toNat u < n }
Equations
@[inline]
def Std.HashMapImp.reinsertAux {α : Type u} {β : Type v} (hashFn : αUInt64) (data : Std.HashMapBucket α β) (a : α) (b : β) :
Equations
@[inline]
def Std.HashMapImp.foldBucketsM {α : Type u} {β : Type v} {δ : Type w} {m : Type wType w} [inst : Monad m] (data : Std.HashMapBucket α β) (d : δ) (f : δαβm δ) :
m δ
Equations
@[inline]
def Std.HashMapImp.foldBuckets {α : Type u} {β : Type v} {δ : Type w} (data : Std.HashMapBucket α β) (d : δ) (f : δαβδ) :
δ
Equations
@[inline]
def Std.HashMapImp.foldM {α : Type u} {β : Type v} {δ : Type w} {m : Type wType w} [inst : Monad m] (f : δαβm δ) (d : δ) (h : Std.HashMapImp α β) :
m δ
Equations
@[inline]
def Std.HashMapImp.fold {α : Type u} {β : Type v} {δ : Type w} (f : δαβδ) (d : δ) (m : Std.HashMapImp α β) :
δ
Equations
@[inline]
def Std.HashMapImp.forBucketsM {α : Type u} {β : Type v} {m : Type wType w} [inst : Monad m] (data : Std.HashMapBucket α β) (f : αβm PUnit) :
Equations
@[inline]
def Std.HashMapImp.forM {α : Type u} {β : Type v} {m : Type wType w} [inst : Monad m] (f : αβm PUnit) (h : Std.HashMapImp α β) :
Equations
def Std.HashMapImp.findEntry? {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] (m : Std.HashMapImp α β) (a : α) :
Option (α × β)
Equations
def Std.HashMapImp.find? {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] (m : Std.HashMapImp α β) (a : α) :
Equations
def Std.HashMapImp.contains {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] (m : Std.HashMapImp α β) (a : α) :
Equations
partial def Std.HashMapImp.moveEntries {α : Type u} {β : Type v} [inst : Hashable α] (i : Nat) (source : Array (Std.AssocList α β)) (target : Std.HashMapBucket α β) :
def Std.HashMapImp.expand {α : Type u} {β : Type v} [inst : Hashable α] (size : Nat) (buckets : Std.HashMapBucket α β) :
Equations
@[inline]
def Std.HashMapImp.insert {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] (m : Std.HashMapImp α β) (a : α) (b : β) :
Equations
def Std.HashMapImp.erase {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] (m : Std.HashMapImp α β) (a : α) :
Equations
inductive Std.HashMapImp.WellFormed {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] :
Std.HashMapImp α βProp
noncomputable def Std.HashMap (α : Type u) (β : Type v) [inst : BEq α] [inst : Hashable α] :
Type (max 0 u v)
Equations
def Std.mkHashMap {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] (capacity : optParam Nat 0) :
Equations
instance Std.HashMap.instInhabitedHashMap {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] :
Equations
  • Std.HashMap.instInhabitedHashMap = { default := Std.mkHashMap }
instance Std.HashMap.instEmptyCollectionHashMap {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] :
Equations
  • Std.HashMap.instEmptyCollectionHashMap = { emptyCollection := Std.mkHashMap }
@[inline]
def Std.HashMap.empty {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] :
Equations
  • Std.HashMap.empty = Std.mkHashMap
def Std.HashMap.insert {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαβStd.HashMap α β
Equations
def Std.HashMap.insert' {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαβStd.HashMap α β × Bool
Equations
@[inline]
def Std.HashMap.erase {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαStd.HashMap α β
Equations
@[inline]
def Std.HashMap.findEntry? {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαOption (α × β)
Equations
@[inline]
def Std.HashMap.find? {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαOption β
Equations
@[inline]
def Std.HashMap.findD {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαββ
Equations
@[inline]
def Std.HashMap.find! {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → [inst : Inhabited β] → Std.HashMap α βαβ
Equations
@[inline]
def Std.HashMap.getOp {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαOption β
Equations
@[inline]
def Std.HashMap.contains {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βαBool
Equations
@[inline]
def Std.HashMap.foldM {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → {δ : Type w} → {m : Type wType w} → [inst : Monad m] → (δαβm δ) → δStd.HashMap α βm δ
Equations
@[inline]
def Std.HashMap.fold {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → {δ : Type w} → (δαβδ) → δStd.HashMap α βδ
Equations
@[inline]
def Std.HashMap.forM {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → {m : Type wType w} → [inst : Monad m] → (αβm PUnit) → Std.HashMap α βm PUnit
Equations
@[inline]
def Std.HashMap.size {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βNat
Equations
  • Std.HashMap.size m = match m with | { val := { size := sz, buckets := x }, property := x_1 } => sz
@[inline]
def Std.HashMap.isEmpty {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βBool
Equations
def Std.HashMap.toList {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βList (α × β)
Equations
def Std.HashMap.toArray {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βArray (α × β)
Equations
def Std.HashMap.numBuckets {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α βNat
Equations
def Std.HashMap.ofList {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → List (α × β)Std.HashMap α β
Equations
def Std.HashMap.ofListWith {α : Type u} {β : Type v} :
{x : BEq α} → {x_1 : Hashable α} → List (α × β)(βββ) → Std.HashMap α β
Equations