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

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

• size : Nat
• buckets : Lean.HashSetBucket α

def Lean.mkHashSetImp {α : Type u} (capacity : optParam 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

• m.find? a = match m with | { size := size, buckets := buckets } => 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

• m.contains a = match m with | { size := size, buckets := buckets } => 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 = let bucketsNew := ⟨mkArray (buckets.val.size * 2) [], ⋯⟩; { size := size, buckets := Lean.HashSetImp.moveEntries 0 buckets.val bucketsNew }

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} [inst : BEq α] [inst_1 : Hashable α] (n : Nat), (Lean.mkHashSetImp n).WellFormed
• insertWff: ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Lean.HashSetImp α) (a : α), m.WellFormed → (m.insert a).WellFormed
• eraseWff: ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Lean.HashSetImp α) (a : α), m.WellFormed → (m.erase a).WellFormed

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

Equations

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

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

Equations

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

@[inline]

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_1 : Hashable α} → Lean.HashSet α → α → Lean.HashSet α

Equations

• m.insert a = match m with | ⟨m, hw⟩ => ⟨m.insert a, ⋯⟩

@[inline]

def Lean.HashSet.erase {α : Type u} : {x : BEq α} → {x_1 : Hashable α} → Lean.HashSet α → α → Lean.HashSet α

Equations

• m.erase a = match m with | ⟨m, hw⟩ => ⟨m.erase a, ⋯⟩

@[inline]

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

Equations

• m.find? a = match m with | ⟨m, property⟩ => m.find? a

@[inline]

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

Equations

• m.contains a = match m with | ⟨m, property⟩ => m.contains a

@[inline]

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

Equations

• Lean.HashSet.foldM f init h = match h with | ⟨h, property⟩ => Lean.HashSetImp.foldM f init h

@[inline]

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

Equations

• Lean.HashSet.fold f init m = match m with | ⟨m, property⟩ => Lean.HashSetImp.fold f init m

@[inline]

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

Equations

• h.forM f = match h with | ⟨h, property⟩ => Lean.HashSetImp.forM f h

instance Lean.HashSet.instForM {α : Type u} : {x : BEq α} → {x_1 : 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_1 : Hashable α} → {m : Type (max u_1 u_2) → Type u_1} → ForIn m (Lean.HashSet α) α

Equations

• Lean.HashSet.instForIn = { forIn := fun {β : Type (max u_1 u_2)} [Monad m] => ForM.forIn }

@[inline]

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

Equations

• m.size = match m with | ⟨{ size := sz, buckets := buckets }, property⟩ => sz

@[inline]

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

Equations

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

def Lean.HashSet.toList {α : Type u} : {x : BEq α} → {x_1 : Hashable α} → 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_1 : Hashable α} → 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_1 : Hashable α} → Lean.HashSet α → Nat

Equations

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

def Lean.HashSet.insertMany {α : Type u} : {x : BEq α} → {x_1 : Hashable α} → {ρ : Type u_1} → [inst : ForIn Id ρ α] → Lean.HashSet α → ρ → 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 : Lean.HashSet α) (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