Documentation

Lean.Data.HashSet

def Lean.HashSetBucket (α : Type u) :
Equations
def Lean.HashSetBucket.update {α : Type u} (data : Lean.HashSetBucket α) (i : USize) (d : List α) (h : i.toNat < data.val.size) :
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) :
@[deprecated Std.HashSet.Raw.empty]
def Lean.mkHashSetImp {α : Type u} (capacity : Nat := 8) :
Equations
@[inline]
def Lean.HashSetImp.reinsertAux {α : Type u} (hashFn : αUInt64) (data : Lean.HashSetBucket α) (a : α) :
Equations
@[inline]
def Lean.HashSetImp.foldBucketsM {α : Type u} {δ : Type w} {m : Type w → Type w} [Monad m] (data : Lean.HashSetBucket α) (d : δ) (f : δαm δ) :
m δ
Equations
@[inline]
def Lean.HashSetImp.foldBuckets {α : Type u} {δ : Type w} (data : Lean.HashSetBucket α) (d : δ) (f : δαδ) :
δ
Equations
@[inline]
def Lean.HashSetImp.foldM {α : Type u} {δ : Type w} {m : Type w → Type w} [Monad m] (f : δαm δ) (d : δ) (h : Lean.HashSetImp α) :
m δ
Equations
@[inline]
def Lean.HashSetImp.fold {α : Type u} {δ : Type w} (f : δαδ) (d : δ) (m : Lean.HashSetImp α) :
δ
Equations
@[inline]
def Lean.HashSetImp.forBucketsM {α : Type u} {m : Type w → Type w} [Monad m] (data : Lean.HashSetBucket α) (f : αm PUnit) :
Equations
@[inline]
def Lean.HashSetImp.forM {α : Type u} {m : Type w → Type w} [Monad m] (f : αm PUnit) (h : Lean.HashSetImp α) :
Equations
def Lean.HashSetImp.find? {α : Type u} [BEq α] [Hashable α] (m : Lean.HashSetImp α) (a : α) :
Equations
def Lean.HashSetImp.contains {α : Type u} [BEq α] [Hashable α] (m : Lean.HashSetImp α) (a : α) :
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 α) :
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 α) :
Equations
def Lean.HashSetImp.insert {α : Type u} [BEq α] [Hashable α] (m : Lean.HashSetImp α) (a : α) :
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 : α) :
Equations
  • One or more equations did not get rendered due to their size.
inductive Lean.HashSetImp.WellFormed {α : Type u} [BEq α] [Hashable α] :
@[deprecated Std.HashSet.empty]
def Lean.mkHashSet {α : Type u} [BEq α] [Hashable α] (capacity : Nat := 8) :
Equations
@[inline, deprecated Std.HashSet.empty]
def Lean.HashSet.empty {α : Type u_1} [BEq α] [Hashable α] :
Equations
  • Lean.HashSet.empty = Lean.mkHashSet
Equations
  • Lean.HashSet.instInhabited = { default := Lean.mkHashSet }
Equations
  • Lean.HashSet.instEmptyCollection = { emptyCollection := Lean.mkHashSet }
@[inline]
def Lean.HashSet.insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashSet α) (a : α) :
Equations
@[inline]
def Lean.HashSet.erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashSet α) (a : α) :
Equations
@[inline]
def Lean.HashSet.find? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashSet α) (a : α) :
Equations
@[inline]
def Lean.HashSet.contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashSet α) (a : α) :
Equations
@[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
@[inline]
def Lean.HashSet.fold {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {δ : Type w} (f : δαδ) (init : δ) (m : Lean.HashSet α) :
δ
Equations
@[inline]
def Lean.HashSet.forM {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Type w → Type w} [Monad m] (h : Lean.HashSet α) (f : αm PUnit) :
Equations
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} :
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 α) :
Equations
@[inline]
def Lean.HashSet.isEmpty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashSet α) :
Equations
def Lean.HashSet.toList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashSet α) :
List α
Equations
def Lean.HashSet.toArray {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashSet α) :
Equations
def Lean.HashSet.numBuckets {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Lean.HashSet α) :
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 : ρ) :

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 α) :

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

Equations