structure Lake.OrdHashSet (α : Type u_1) [Hashable α] [BEq α] : Type u_1

A HashSet that preserves insertion order.

• toHashSet : Lean.HashSet α
• toArray : Array α

instance Lake.OrdHashSet.instCoeOrdHashSetHashSet {α : Type u_1} [Hashable α] [BEq α] : Coe (Lake.OrdHashSet α) (Lean.HashSet α)

Equations

• Lake.OrdHashSet.instCoeOrdHashSetHashSet = { coe := Lake.OrdHashSet.toHashSet }

def Lake.OrdHashSet.empty {α : Type u_1} [Hashable α] [BEq α] : Lake.OrdHashSet α

Equations

• Lake.OrdHashSet.empty = { toHashSet := Lean.HashSet.empty, toArray := #[] }

instance Lake.OrdHashSet.instEmptyCollectionOrdHashSet {α : Type u_1} [Hashable α] [BEq α] : EmptyCollection (Lake.OrdHashSet α)

Equations

• Lake.OrdHashSet.instEmptyCollectionOrdHashSet = { emptyCollection := Lake.OrdHashSet.empty }

def Lake.OrdHashSet.mkEmpty {α : Type u_1} [Hashable α] [BEq α] (size : Nat) : Lake.OrdHashSet α

Equations

• Lake.OrdHashSet.mkEmpty size = { toHashSet := Lean.HashSet.empty, toArray := Array.mkEmpty size }

def Lake.OrdHashSet.insert {α : Type u_1} [Hashable α] [BEq α] (self : Lake.OrdHashSet α) (a : α) : Lake.OrdHashSet α

Equations

• Lake.OrdHashSet.insert self a = if Lean.HashSet.contains self.toHashSet a = true then self else { toHashSet := Lean.HashSet.insert self.toHashSet a, toArray := Array.push self.toArray a }

def Lake.OrdHashSet.appendArray {α : Type u_1} [Hashable α] [BEq α] (self : Lake.OrdHashSet α) (arr : Array α) : Lake.OrdHashSet α

Equations

• Lake.OrdHashSet.appendArray self arr = Array.foldl (fun (x : Lake.OrdHashSet α) (x_1 : α) => Lake.OrdHashSet.insert x x_1) self arr 0

instance Lake.OrdHashSet.instHAppendOrdHashSetArray {α : Type u_1} [Hashable α] [BEq α] : HAppend (Lake.OrdHashSet α) (Array α) (Lake.OrdHashSet α)

Equations

• Lake.OrdHashSet.instHAppendOrdHashSetArray = { hAppend := Lake.OrdHashSet.appendArray }

def Lake.OrdHashSet.append {α : Type u_1} [Hashable α] [BEq α] (self : Lake.OrdHashSet α) (other : Lake.OrdHashSet α) : Lake.OrdHashSet α

Equations

• Lake.OrdHashSet.append self other = Lake.OrdHashSet.appendArray self other.toArray

instance Lake.OrdHashSet.instAppendOrdHashSet {α : Type u_1} [Hashable α] [BEq α] : Append (Lake.OrdHashSet α)

Equations

• Lake.OrdHashSet.instAppendOrdHashSet = { append := Lake.OrdHashSet.append }

def Lake.OrdHashSet.ofArray {α : Type u_1} [Hashable α] [BEq α] (arr : Array α) : Lake.OrdHashSet α

Equations

• Lake.OrdHashSet.ofArray arr = Lake.OrdHashSet.appendArray (Lake.OrdHashSet.mkEmpty (Array.size arr)) arr

@[inline]

def Lake.OrdHashSet.all {α : Type u_1} [Hashable α] [BEq α] (f : α → Bool) (self : Lake.OrdHashSet α) : Bool

Equations

• Lake.OrdHashSet.all f self = Array.all self.toArray f 0

@[inline]

def Lake.OrdHashSet.any {α : Type u_1} [Hashable α] [BEq α] (f : α → Bool) (self : Lake.OrdHashSet α) : Bool

Equations

• Lake.OrdHashSet.any f self = Array.any self.toArray f 0

@[inline]

def Lake.OrdHashSet.foldl {α : Type u_1} [Hashable α] [BEq α] {β : Type u_2} (f : β → α → β) (init : β) (self : Lake.OrdHashSet α) : β

Equations

• Lake.OrdHashSet.foldl f init self = Array.foldl f init self.toArray 0

@[inline]

def Lake.OrdHashSet.foldlM {α : Type u_1} [Hashable α] [BEq α] {m : Type u_2 → Type u_3} {β : Type u_2} [Monad m] (f : β → α → m β) (init : β) (self : Lake.OrdHashSet α) : m β

Equations

• Lake.OrdHashSet.foldlM f init self = Array.foldlM f init self.toArray 0

@[inline]

def Lake.OrdHashSet.foldr {α : Type u_1} [Hashable α] [BEq α] {β : Type u_2} (f : α → β → β) (init : β) (self : Lake.OrdHashSet α) : β

Equations

• Lake.OrdHashSet.foldr f init self = Array.foldr f init self.toArray (Array.size self.toArray)

@[inline]

def Lake.OrdHashSet.foldrM {α : Type u_1} [Hashable α] [BEq α] {m : Type u_2 → Type u_3} {β : Type u_2} [Monad m] (f : α → β → m β) (init : β) (self : Lake.OrdHashSet α) : m β

Equations

• Lake.OrdHashSet.foldrM f init self = Array.foldrM f init self.toArray (Array.size self.toArray)

@[inline]

def Lake.OrdHashSet.forM {α : Type u_1} [Hashable α] [BEq α] {m : Type u_2 → Type u_3} [Monad m] (f : α → m PUnit) (self : Lake.OrdHashSet α) : m PUnit

Equations

• Lake.OrdHashSet.forM f self = Array.forM f self.toArray 0

@[inline]

def Lake.OrdHashSet.forIn {α : Type u_1} [Hashable α] [BEq α] {m : Type u_2 → Type u_3} {β : Type u_2} [Monad m] (self : Lake.OrdHashSet α) (init : β) (f : α → β → m (ForInStep β)) : m β

Equations

• Lake.OrdHashSet.forIn self init f = Array.forIn self.toArray init f

instance Lake.OrdHashSet.instForInOrdHashSet {α : Type u_1} [Hashable α] [BEq α] {m : Type u_2 → Type u_3} : ForIn m (Lake.OrdHashSet α) α

Equations

• Lake.OrdHashSet.instForInOrdHashSet = { forIn := fun {β : Type u_2} [Monad m] => Lake.OrdHashSet.forIn }