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

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

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

• size : Nat
• buckets : Lean.HashSetBucket α

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

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

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

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 α

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

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

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

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

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

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

@[inline]

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

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

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

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

@[inline]

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

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

instance Lean.HashSet.instForMHashSet {α : Type u} : {x : BEq α} → {x_1 : Hashable α} → {m : Type u_1 → Type u_1} → ForM m (Lean.HashSet α) α

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

@[inline]

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

@[inline]

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

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

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

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

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.