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

Equations

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

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

Equations

• Lean.HashSetBucket.update data i d h = { val := Array.uset data.val i d h, property := (_ : Nat.isPowerOfTwo (Array.size (Array.uset data.val i d h))) }

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

• size : Nat
• buckets : Lean.HashSetBucket α

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

Equations

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

@[inline]

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

Equations

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

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

@[inline]

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

Equations

• Lean.HashSetImp.foldBuckets data d f = Id.run (Lean.HashSetImp.foldBucketsM data 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 δ

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 α) => List.forM as f) data.val 0

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

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

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

Equations

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

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

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

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.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

Equations

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

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

Equations

• Lean.mkHashSet capacity = { val := Lean.mkHashSetImp capacity, property := (_ : Lean.HashSetImp.WellFormed (Lean.mkHashSetImp capacity)) }

@[inline]

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

Equations

• Lean.HashSet.empty = Lean.mkHashSet

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

Equations

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

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

Equations

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

@[inline]

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

Equations

• Lean.HashSet.insert m a = match m with | { val := m, property := hw } => { val := Lean.HashSetImp.insert m a, property := (_ : Lean.HashSetImp.WellFormed (Lean.HashSetImp.insert m a)) }

@[inline]

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

Equations

• Lean.HashSet.erase m a = match m with | { val := m, property := hw } => { val := Lean.HashSetImp.erase m a, property := (_ : Lean.HashSetImp.WellFormed (Lean.HashSetImp.erase m a)) }

@[inline]

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

Equations

• Lean.HashSet.find? m a = match m with | { val := m, property := property } => Lean.HashSetImp.find? m a

@[inline]

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

Equations

• Lean.HashSet.contains m a = match m with | { val := m, property := property } => Lean.HashSetImp.contains m 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 | { val := h, property := 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 | { val := m, property := 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

• Lean.HashSet.forM h f = match h with | { val := h, property := property } => Lean.HashSetImp.forM f h

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

Equations

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

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

Equations

• Lean.HashSet.instForInHashSet = { 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

• Lean.HashSet.size m = match m with | { val := { size := sz, buckets := buckets }, property := property } => sz

@[inline]

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

Equations

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

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

Equations

• Lean.HashSet.toList m = 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

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

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

Equations

• Lean.HashSet.numBuckets m = Array.size m.val.buckets.val

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.