def Lean.HashSetBucket (α : Type u) : Type u

Equations

• Lean.HashSetBucket α = { b : Array (List α) // b.size.isPowerOfTwo }

def Lean.HashSetBucket.update {α : Type u} (data : Lean.HashSetBucket α) (i : USize) (d : List α) (h : i.toNat < data.val.size) : Lean.HashSetBucket α

Equations

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

@[simp]

theorem Lean.HashSetBucket.size_update {α : Type u} (data : Lean.HashSetBucket α) (i : USize) (d : List α) (h : i.toNat < data.val.size) : (data.update i d h).val.size = data.val.size

@[deprecated Std.HashSet.Raw]

structure Lean.HashSetImp (α : Type u) : Type u

• size : Nat
• buckets : Lean.HashSetBucket α

@[deprecated Std.HashSet.Raw.empty]

def Lean.mkHashSetImp {α : Type u} (capacity : Nat := 8) : Lean.HashSetImp α

Equations

• Lean.mkHashSetImp capacity = { size := 0, buckets := ⟨mkArray (Nat.nextPowerOfTwo (capacity * 4 / 3)) [], ⋯⟩ }

@[inline]

def Lean.HashSetImp.reinsertAux {α : Type u} (hashFn : α → UInt64) (data : Lean.HashSetBucket α) (a : α) : Lean.HashSetBucket α

Equations

• Lean.HashSetImp.reinsertAux hashFn data a = match Lean.HashSetImp.mkIdx✝ (hashFn a) ⋯ with | ⟨i, h⟩ => data.update i (a :: data.val[i]) h

@[inline]

def Lean.HashSetImp.foldBucketsM {α : Type u} {δ : Type w} {m : Type w → Type w} [Monad m] (data : Lean.HashSetBucket α) (d : δ) (f : δ → α → m δ) : m δ

Equations

• Lean.HashSetImp.foldBucketsM data d f = Array.foldlM (fun (d : δ) (as : List α) => List.foldlM f d as) d data.val

@[inline]

def Lean.HashSetImp.foldBuckets {α : Type u} {δ : Type w} (data : Lean.HashSetBucket α) (d : δ) (f : δ → α → δ) : δ

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

def Lean.HashSetImp.forBucketsM {α : Type u} {m : Type w → Type w} [Monad m] (data : Lean.HashSetBucket α) (f : α → m PUnit) : m PUnit

Equations

• Lean.HashSetImp.forBucketsM data f = Array.forM (fun (as : List α) => as.forM f) data.val

@[inline]

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

Equations

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

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

Equations

• { size := size, buckets := buckets }.find? a = match Lean.HashSetImp.mkIdx✝ (hash a) ⋯ with | ⟨i, h⟩ => List.find? (fun (a' : α) => a == a') buckets.val[i]

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

Equations

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

@[irreducible]

def Lean.HashSetImp.moveEntries {α : Type u} [Hashable α] (i : Nat) (source : Array (List α)) (target : Lean.HashSetBucket α) : Lean.HashSetBucket α

Equations

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

def Lean.HashSetImp.expand {α : Type u} [Hashable α] (size : Nat) (buckets : Lean.HashSetBucket α) : Lean.HashSetImp α

Equations

• Lean.HashSetImp.expand size buckets = { size := size, buckets := Lean.HashSetImp.moveEntries 0 buckets.val ⟨mkArray (buckets.val.size * 2) [], ⋯⟩ }

def Lean.HashSetImp.insert {α : Type u} [BEq α] [Hashable α] (m : Lean.HashSetImp α) (a : α) : Lean.HashSetImp α

Equations

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

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

Equations

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

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

• mkWff {α : Type u} [BEq α] [Hashable α] (n : Nat) : (Lean.mkHashSetImp n).WellFormed
• insertWff {α : Type u} [BEq α] [Hashable α] (m : Lean.HashSetImp α) (a : α) : m.WellFormed → (m.insert a).WellFormed
• eraseWff {α : Type u} [BEq α] [Hashable α] (m : Lean.HashSetImp α) (a : α) : m.WellFormed → (m.erase a).WellFormed

@[deprecated Std.HashSet]

def Lean.HashSet (α : Type u) [BEq α] [Hashable α] : Type u

Equations

• Lean.HashSet α = { m : Lean.HashSetImp α // m.WellFormed }

@[deprecated Std.HashSet.empty]

def Lean.mkHashSet {α : Type u} [BEq α] [Hashable α] (capacity : Nat := 8) : Lean.HashSet α

Equations

• Lean.mkHashSet capacity = ⟨Lean.mkHashSetImp capacity, ⋯⟩

@[inline, deprecated Std.HashSet.empty]

def Lean.HashSet.empty {α : Type u_1} [BEq α] [Hashable α] : Lean.HashSet α

Equations

• Lean.HashSet.empty = Lean.mkHashSet

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

Equations

• Lean.HashSet.instInhabited = { default := Lean.mkHashSet }

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

Equations

• Lean.HashSet.instEmptyCollection = { emptyCollection := Lean.mkHashSet }

@[inline]

def Lean.HashSet.insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashSet α) (a : α) : Lean.HashSet α

Equations

• Lean.HashSet.insert ⟨m_2, hw⟩ a = ⟨m_2.insert a, ⋯⟩

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

def Lean.HashSet.foldM {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → m δ) (init : δ) (h : Lean.HashSet α) : m δ

Equations

• Lean.HashSet.foldM f init ⟨m_2, hw⟩ = Lean.HashSetImp.foldM f init m_2

@[inline]

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

Equations

• Lean.HashSet.fold f init ⟨m_2, hw⟩ = Lean.HashSetImp.fold f init m_2

@[inline]

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

Equations

• Lean.HashSet.forM ⟨m_2, hw⟩ f = Lean.HashSetImp.forM f m_2

instance Lean.HashSet.instForM {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Type u_1 → Type u_1} : ForM m (Lean.HashSet α) α

Equations

• Lean.HashSet.instForM = { forM := fun [Monad m] => Lean.HashSet.forM }

instance Lean.HashSet.instForIn {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Type (max u_1 u_2) → Type u_1} : ForIn m (Lean.HashSet α) α

Equations

• Lean.HashSet.instForIn = { forIn := fun {β : Type (max ?u.32 ?u.31)} [Monad m] => ForM.forIn }

@[inline]

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

Equations

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

@[inline]

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

Equations

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

def Lean.HashSet.toList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashSet α) : List α

Equations

• m.toList = Lean.HashSet.fold (fun (r : List α) (a : α) => a :: r) [] m

def Lean.HashSet.toArray {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashSet α) : Array α

Equations

• m.toArray = Lean.HashSet.fold (fun (r : Array α) (a : α) => r.push a) #[] m

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

Equations

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

def Lean.HashSet.insertMany {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {ρ : Type u_1} [ForIn Id ρ α] (s : Lean.HashSet α) (as : ρ) : Lean.HashSet α

Insert many elements into a HashSet.

Equations

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

@[inline]

def Lean.HashSet.merge {α : Type u} [BEq α] [Hashable α] (s t : Lean.HashSet α) : Lean.HashSet α

O(|t|) amortized. Merge two HashSets.

Equations

• s.merge t = Lean.HashSet.fold (fun (s : Lean.HashSet α) (a : α) => s.insert a) s t