def Lean.HashMapBucket (α : Type u) (β : Type v) : Type (max 0 u v)

def Lean.HashMapBucket.update {α : Type u} {β : Type v} (data : Lean.HashMapBucket α β) (i : USize) (d : Lean.AssocList α β) (h : USize.toNat i < Array.size data.val) : Lean.HashMapBucket α β

structure Lean.HashMapImp (α : Type u) (β : Type v) : Type (max u v)

• size : Nat
• buckets : Lean.HashMapBucket α β

def Lean.mkHashMapImp {α : Type u} {β : Type v} (capacity : optParam Nat 8) : Lean.HashMapImp α β

@[inline]

def Lean.HashMapImp.reinsertAux {α : Type u} {β : Type v} (hashFn : α → UInt64) (data : Lean.HashMapBucket α β) (a : α) (b : β) : Lean.HashMapBucket α β

@[inline]

def Lean.HashMapImp.foldBucketsM {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Monad m] (data : Lean.HashMapBucket α β) (d : δ) (f : δ → α → β → m δ) : m δ

@[inline]

def Lean.HashMapImp.foldBuckets {α : Type u} {β : Type v} {δ : Type w} (data : Lean.HashMapBucket α β) (d : δ) (f : δ → α → β → δ) : δ

@[inline]

def Lean.HashMapImp.foldM {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → β → m δ) (d : δ) (h : Lean.HashMapImp α β) : m δ

@[inline]

def Lean.HashMapImp.fold {α : Type u} {β : Type v} {δ : Type w} (f : δ → α → β → δ) (d : δ) (m : Lean.HashMapImp α β) : δ

@[inline]

def Lean.HashMapImp.forBucketsM {α : Type u} {β : Type v} {m : Type w → Type w} [Monad m] (data : Lean.HashMapBucket α β) (f : α → β → m PUnit) : m PUnit

@[inline]

def Lean.HashMapImp.forM {α : Type u} {β : Type v} {m : Type w → Type w} [Monad m] (f : α → β → m PUnit) (h : Lean.HashMapImp α β) : m PUnit

def Lean.HashMapImp.findEntry? {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.HashMapImp α β) (a : α) : Option (α × β)

def Lean.HashMapImp.find? {α : Type u} {β : Type v} [beq : BEq α] [Hashable α] (m : Lean.HashMapImp α β) (a : α) : Option β

def Lean.HashMapImp.contains {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.HashMapImp α β) (a : α) : Bool

def Lean.HashMapImp.moveEntries {α : Type u} {β : Type v} [Hashable α] (i : Nat) (source : Array (Lean.AssocList α β)) (target : Lean.HashMapBucket α β) : Lean.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 : Lean.HashMapBucket α β) : Lean.HashMapImp α β

@[inline]

def Lean.HashMapImp.insert {α : Type u} {β : Type v} [beq : BEq α] [Hashable α] (m : Lean.HashMapImp α β) (a : α) (b : β) : Lean.HashMapImp α β × Bool

def Lean.HashMapImp.erase {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.HashMapImp α β) (a : α) : Lean.HashMapImp α β

inductive Lean.HashMapImp.WellFormed {α : Type u} {β : Type v} [BEq α] [Hashable α] : Lean.HashMapImp α β → Prop

• mkWff: ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (n : Nat), Lean.HashMapImp.WellFormed (Lean.mkHashMapImp n)
• insertWff: ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Lean.HashMapImp α β) (a : α) (b : β), Lean.HashMapImp.WellFormed m → Lean.HashMapImp.WellFormed (Lean.HashMapImp.insert m a b).fst
• eraseWff: ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Lean.HashMapImp α β) (a : α), Lean.HashMapImp.WellFormed m → Lean.HashMapImp.WellFormed (Lean.HashMapImp.erase m a)

def Lean.HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] : Type (max 0 u v)

def Lean.mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (capacity : optParam Nat 8) : Lean.HashMap α β

instance Lean.HashMap.instInhabitedHashMap {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] : Inhabited (Lean.HashMap α β)

instance Lean.HashMap.instEmptyCollectionHashMap {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] : EmptyCollection (Lean.HashMap α β)

@[inline]

def Lean.HashMap.empty {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] : Lean.HashMap α β

def Lean.HashMap.insert {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α β → α → β → Lean.HashMap α β

def Lean.HashMap.insert' {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α β → α → β → Lean.HashMap α β × Bool

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

@[inline]

def Lean.HashMap.erase {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α β → α → Lean.HashMap α β

@[inline]

def Lean.HashMap.findEntry? {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α β → α → Option (α × β)

@[inline]

def Lean.HashMap.find? {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α β → α → Option β

@[inline]

def Lean.HashMap.findD {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α β → α → β → β

@[inline]

def Lean.HashMap.find! {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → [inst : Inhabited β] → Lean.HashMap α β → α → β

instance Lean.HashMap.instGetElemHashMapOptionTrue {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → GetElem (Lean.HashMap α β) α (Option β) fun x x => True

@[inline]

def Lean.HashMap.contains {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α β → α → Bool

@[inline]

def Lean.HashMap.foldM {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → {δ : Type w} → {m : Type w → Type w} → [inst : Monad m] → (δ → α → β → m δ) → δ → Lean.HashMap α β → m δ

@[inline]

def Lean.HashMap.fold {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → {δ : Type w} → (δ → α → β → δ) → δ → Lean.HashMap α β → δ

@[inline]

def Lean.HashMap.forM {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → {m : Type w → Type w} → [inst : Monad m] → (α → β → m PUnit) → Lean.HashMap α β → m PUnit

@[inline]

def Lean.HashMap.size {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α β → Nat

@[inline]

def Lean.HashMap.isEmpty {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α β → Bool

def Lean.HashMap.toList {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α β → List (α × β)

def Lean.HashMap.toArray {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α β → Array (α × β)

def Lean.HashMap.numBuckets {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α β → Nat

def Lean.HashMap.ofList {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → List (α × β) → Lean.HashMap α β

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

def Lean.HashMap.ofListWith {α : Type u} {β : Type v} : {x : BEq α} → {x_1 : Hashable α} → List (α × β) → (β → β → β) → Lean.HashMap α β

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