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

Equations

• Lean.HashMapBucket α β = { b : Array (Lean.AssocList α β) // b.size.isPowerOfTwo }

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

Equations

• data.update i d h = ⟨data.val.uset i d h, ⋯⟩

@[simp]

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

@[deprecated Std.HashMap.Raw]

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

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

@[deprecated Std.HashMap.Raw.empty]

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

Equations

• Lean.mkHashMapImp capacity = { size := 0, buckets := ⟨mkArray (Lean.numBucketsForCapacity capacity).nextPowerOfTwo Lean.AssocList.nil, ⋯⟩ }

@[inline]

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

Equations

• Lean.HashMapImp.reinsertAux hashFn data a b = match Lean.HashMapImp.mkIdx (hashFn a) ⋯ with | ⟨i, h⟩ => data.update i (Lean.AssocList.cons a b data.val[i]) h

@[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 δ

Equations

• Lean.HashMapImp.foldBucketsM data d f = Array.foldlM (fun (d : δ) (b : Lean.AssocList α β) => Lean.AssocList.foldlM f d b) d data.val

@[inline]

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

Equations

• Lean.HashMapImp.foldBuckets data d f = (Lean.HashMapImp.foldBucketsM data d f).run

@[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 δ

Equations

• Lean.HashMapImp.foldM f d h = Lean.HashMapImp.foldBucketsM h.buckets d f

@[inline]

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

Equations

• Lean.HashMapImp.fold f d m = Lean.HashMapImp.foldBuckets m.buckets d f

@[inline]

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

Equations

• Lean.HashMapImp.forBucketsM data f = Array.forM (fun (b : Lean.AssocList α β) => Lean.AssocList.forM f b) data.val

@[inline]

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

Equations

• Lean.HashMapImp.forM f h = Lean.HashMapImp.forBucketsM h.buckets f

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

Equations

• { size := size, buckets := buckets }.findEntry? a = match Lean.HashMapImp.mkIdx (hash a) ⋯ with | ⟨i, h⟩ => Lean.AssocList.findEntry? a buckets.val[i]

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

Equations

• { size := size, buckets := buckets }.find? a = match Lean.HashMapImp.mkIdx (hash a) ⋯ with | ⟨i, h⟩ => Lean.AssocList.find? a buckets.val[i]

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

Equations

• { size := size, buckets := buckets }.contains a = match Lean.HashMapImp.mkIdx (hash a) ⋯ with | ⟨i, h⟩ => Lean.AssocList.contains a buckets.val[i]

@[irreducible]

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 α β

Equations

• Lean.HashMapImp.expand size buckets = { size := size, buckets := Lean.HashMapImp.moveEntries 0 buckets.val ⟨mkArray (buckets.val.size * 2) Lean.AssocList.nil, ⋯⟩ }

@[inline]

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

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 : Lean.HashMapImp α β) (a : α) (b : β) : Lean.HashMapImp α β × Option β

Equations

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

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

Equations

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

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.mkHashMapImp n).WellFormed
• insertWff: ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Lean.HashMapImp α β) (a : α) (b : β), m.WellFormed → (m.insert a b).fst.WellFormed
• insertIfNewWff: ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Lean.HashMapImp α β) (a : α) (b : β), m.WellFormed → (m.insertIfNew a b).fst.WellFormed
• eraseWff: ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Lean.HashMapImp α β) (a : α), m.WellFormed → (m.erase a).WellFormed

@[deprecated Std.HashMap]

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

Equations

• Lean.HashMap α β = { m : Lean.HashMapImp α β // m.WellFormed }

@[deprecated Std.HashMap.empty]

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

Equations

• Lean.mkHashMap capacity = ⟨Lean.mkHashMapImp capacity, ⋯⟩

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

Equations

• Lean.HashMap.instInhabited = { default := Lean.mkHashMap }

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

Equations

• Lean.HashMap.instEmptyCollection = { emptyCollection := Lean.mkHashMap }

@[inline, deprecated Std.HashMap.empty]

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

Equations

• Lean.HashMap.empty = Lean.mkHashMap

def Lean.HashMap.insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashMap α β) (a : α) (b : β) : Lean.HashMap α β

Equations

• Lean.HashMap.insert ⟨m_2, hw⟩ a b = match h : m_2.insert a b with | (m', snd) => ⟨m', ⋯⟩

def Lean.HashMap.insert' {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashMap α β) (a : α) (b : β) : Lean.HashMap α β × Bool

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

Equations

• Lean.HashMap.insert' ⟨m_2, hw⟩ a b = match h : m_2.insert a b with | (m', replaced) => (⟨m', ⋯⟩, replaced)

def Lean.HashMap.insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashMap α β) (a : α) (b : β) : Lean.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

• Lean.HashMap.insertIfNew ⟨m_2, hw⟩ a b = match h : m_2.insertIfNew a b with | (m', old) => (⟨m', ⋯⟩, old)

@[inline]

def Lean.HashMap.erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashMap α β) (a : α) : Lean.HashMap α β

Equations

• Lean.HashMap.erase ⟨m_2, hw⟩ a = ⟨m_2.erase a, ⋯⟩

@[inline]

def Lean.HashMap.findEntry? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashMap α β) (a : α) : Option (α × β)

Equations

• Lean.HashMap.findEntry? ⟨m_2, hw⟩ a = m_2.findEntry? a

@[inline]

def Lean.HashMap.find? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashMap α β) (a : α) : Option β

Equations

• Lean.HashMap.find? ⟨m_2, hw⟩ a = m_2.find? a

@[inline]

def Lean.HashMap.findD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashMap α β) (a : α) (b₀ : β) : β

Equations

• m.findD a b₀ = (m.find? a).getD b₀

@[inline]

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

Equations

• m.find! a = match m.find? a with | some b => b | none => panicWithPosWithDecl "Lean.Data.HashMap" "Lean.HashMap.find!" 223 14 "key is not in the map"

instance Lean.HashMap.instGetElemOptionTrue {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} : GetElem (Lean.HashMap α β) α (Option β) fun (x : Lean.HashMap α β) (x : α) => True

Equations

• Lean.HashMap.instGetElemOptionTrue = { getElem := fun (m : Lean.HashMap α β) (k : α) (x_1 : True) => m.find? k }

@[inline]

def Lean.HashMap.contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashMap α β) (a : α) : Bool

Equations

• Lean.HashMap.contains ⟨m_2, hw⟩ a = m_2.contains a

@[inline]

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 : Lean.HashMap α β) : m δ

Equations

• Lean.HashMap.foldM f init ⟨m_2, hw⟩ = Lean.HashMapImp.foldM f init m_2

@[inline]

def Lean.HashMap.fold {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {δ : Type w} (f : δ → α → β → δ) (init : δ) (m : Lean.HashMap α β) : δ

Equations

• Lean.HashMap.fold f init ⟨m_2, hw⟩ = Lean.HashMapImp.fold f init m_2

@[inline]

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

Equations

• Lean.HashMap.forM f ⟨m_2, hw⟩ = Lean.HashMapImp.forM f m_2

@[inline]

def Lean.HashMap.size {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashMap α β) : Nat

Equations

• Lean.HashMap.size ⟨{ size := sz, buckets := buckets }, property⟩ = sz

@[inline]

def Lean.HashMap.isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashMap α β) : Bool

Equations

• m.isEmpty = decide (m.size = 0)

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

Equations

• m.toList = Lean.HashMap.fold (fun (r : List (α × β)) (k : α) (v : β) => (k, v) :: r) [] m

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

Equations

• m.toArray = Lean.HashMap.fold (fun (r : Array (α × β)) (k : α) (v : β) => r.push (k, v)) #[] m

def Lean.HashMap.numBuckets {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashMap α β) : Nat

Equations

• m.numBuckets = m.val.buckets.val.size

@[deprecated Std.HashMap.ofList]

def Lean.HashMap.ofList {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) : Lean.HashMap α β

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

Equations

• Lean.HashMap.ofList l = List.foldl (fun (m : Lean.HashMap α β) (p : α × β) => m.insert p.fst p.snd) Lean.HashMap.empty l

def Lean.HashMap.ofListWith {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) (f : β → β → β) : Lean.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.