structure Aesop.UnorderedArraySet (α : Type u_1) [BEq α] : Type u_1

• rep : Array α

instance Aesop.instInhabitedUnorderedArraySet : {a : Type u_1} → {a_1 : BEq a} → Inhabited (Aesop.UnorderedArraySet a)

Equations

• Aesop.instInhabitedUnorderedArraySet = { default := { rep := default } }

def Aesop.UnorderedArraySet.empty {α : Type u_1} [BEq α] : Aesop.UnorderedArraySet α

O(1)

Equations

• Aesop.UnorderedArraySet.empty = { rep := #[] }

instance Aesop.UnorderedArraySet.instEmptyCollectionUnorderedArraySet {α : Type u_1} [BEq α] : EmptyCollection (Aesop.UnorderedArraySet α)

Equations

• Aesop.UnorderedArraySet.instEmptyCollectionUnorderedArraySet = { emptyCollection := Aesop.UnorderedArraySet.empty }

def Aesop.UnorderedArraySet.singleton {α : Type u_1} [BEq α] (a : α) : Aesop.UnorderedArraySet α

O(1)

Equations

• Aesop.UnorderedArraySet.singleton a = { rep := #[a] }

def Aesop.UnorderedArraySet.insert {α : Type u_1} [BEq α] (x : α) : Aesop.UnorderedArraySet α → Aesop.UnorderedArraySet α

O(n)

Equations

• Aesop.UnorderedArraySet.insert x x = match x with | { rep := rep } => if Array.contains rep x = true then { rep := rep } else { rep := Array.push rep x }

def Aesop.UnorderedArraySet.ofDeduplicatedArray {α : Type u_1} [BEq α] (xs : Array α) : Aesop.UnorderedArraySet α

Precondition: xs contains no duplicates.

Equations

• Aesop.UnorderedArraySet.ofDeduplicatedArray xs = { rep := xs }

def Aesop.UnorderedArraySet.ofSortedArray {α : Type u_1} [BEq α] (xs : Array α) : Aesop.UnorderedArraySet α

Precondition: xs is sorted.

Equations

• Aesop.UnorderedArraySet.ofSortedArray xs = { rep := Array.deduplicateSorted xs }

def Aesop.UnorderedArraySet.ofArray {α : Type u_1} [BEq α] [ord : Ord α] [Inhabited α] (xs : Array α) : Aesop.UnorderedArraySet α

O(n*log(n))

Equations

• Aesop.UnorderedArraySet.ofArray xs = { rep := Array.sortAndDeduplicate xs }

def Aesop.UnorderedArraySet.ofArraySlow {α : Type u_1} [BEq α] (xs : Array α) : Aesop.UnorderedArraySet α

O(n^2)

Equations

• Aesop.UnorderedArraySet.ofArraySlow xs = Array.foldl (fun s x => Aesop.UnorderedArraySet.insert x s) ∅ xs 0 (Array.size xs)

def Aesop.UnorderedArraySet.ofHashSet {α : Type u_1} [BEq α] [Hashable α] (xs : Lean.HashSet α) : Aesop.UnorderedArraySet α

Equations

• Aesop.UnorderedArraySet.ofHashSet xs = { rep := Lean.HashSet.toArray xs }

def Aesop.UnorderedArraySet.ofPersistentHashSet {α : Type u_1} [BEq α] [Hashable α] (xs : Lean.PersistentHashSet α) : Aesop.UnorderedArraySet α

Equations

• Aesop.UnorderedArraySet.ofPersistentHashSet xs = { rep := Lean.PersistentHashSet.fold (fun as a => Array.push as a) (Array.mkEmpty (Lean.PersistentHashSet.size xs)) xs }

def Aesop.UnorderedArraySet.toArray {α : Type u_1} [BEq α] (s : Aesop.UnorderedArraySet α) : Array α

Equations

• Aesop.UnorderedArraySet.toArray s = s.rep

def Aesop.UnorderedArraySet.erase {α : Type u_1} [BEq α] (x : α) (s : Aesop.UnorderedArraySet α) : Aesop.UnorderedArraySet α

O(n)

Equations

• Aesop.UnorderedArraySet.erase x s = { rep := Array.erase s.rep x }

def Aesop.UnorderedArraySet.filterM {α : Type} [BEq α] {m : Type → Type u_1} [Monad m] (p : α → m Bool) (s : Aesop.UnorderedArraySet α) : m (Aesop.UnorderedArraySet α)

O(n)

Equations

• Aesop.UnorderedArraySet.filterM p s = do let __do_lift ← Array.filterM p s.rep 0 (Array.size s.rep) pure { rep := __do_lift }

def Aesop.UnorderedArraySet.filter {α : Type u_1} [BEq α] (p : α → Bool) (s : Aesop.UnorderedArraySet α) : Aesop.UnorderedArraySet α

O(n)

Equations

• Aesop.UnorderedArraySet.filter p s = { rep := Array.filter p s.rep 0 (Array.size s.rep) }

def Aesop.UnorderedArraySet.merge {α : Type u_1} [BEq α] (s : Aesop.UnorderedArraySet α) (t : Aesop.UnorderedArraySet α) : Aesop.UnorderedArraySet α

O(n*m)

Equations

• Aesop.UnorderedArraySet.merge s t = { rep := Array.mergeUnsortedDeduplicating s.rep t.rep }

instance Aesop.UnorderedArraySet.instAppendUnorderedArraySet {α : Type u_1} [BEq α] : Append (Aesop.UnorderedArraySet α)

Equations

• Aesop.UnorderedArraySet.instAppendUnorderedArraySet = { append := Aesop.UnorderedArraySet.merge }

def Aesop.UnorderedArraySet.contains {α : Type u_1} [BEq α] (x : α) (s : Aesop.UnorderedArraySet α) : Bool

O(n)

Equations

• Aesop.UnorderedArraySet.contains x s = Array.contains s.rep x

def Aesop.UnorderedArraySet.foldM {α : Type u_1} [BEq α] {m : Type u_2 → Type u_3} {σ : Type u_2} [Monad m] (f : σ → α → m σ) (init : σ) (s : Aesop.UnorderedArraySet α) : m σ

O(n)

Equations

• Aesop.UnorderedArraySet.foldM f init s = Array.foldlM f init s.rep 0 (Array.size s.rep)

instance Aesop.UnorderedArraySet.instForInUnorderedArraySet {α : Type u_1} [BEq α] {m : Type u_2 → Type u_3} [Monad m] : ForIn m (Aesop.UnorderedArraySet α) α

Equations

• Aesop.UnorderedArraySet.instForInUnorderedArraySet = { forIn := fun {β} [Monad m] s => Array.forIn s.rep }

def Aesop.UnorderedArraySet.fold {α : Type u_1} [BEq α] {σ : Type u_2} (f : σ → α → σ) (init : σ) (s : Aesop.UnorderedArraySet α) : σ

O(n)

Equations

• Aesop.UnorderedArraySet.fold f init s = Array.foldl f init s.rep 0 (Array.size s.rep)

def Aesop.UnorderedArraySet.partition {α : Type u_1} [BEq α] (f : α → Bool) (s : Aesop.UnorderedArraySet α) : Aesop.UnorderedArraySet α × Aesop.UnorderedArraySet α

Equations

• Aesop.UnorderedArraySet.partition f s = match Array.partition f s.rep with | (xs, ys) => ({ rep := xs }, { rep := ys })

def Aesop.UnorderedArraySet.size {α : Type u_1} [BEq α] (s : Aesop.UnorderedArraySet α) : Nat

O(1)

Equations

• Aesop.UnorderedArraySet.size s = Array.size s.rep

def Aesop.UnorderedArraySet.isEmpty {α : Type u_1} [BEq α] (s : Aesop.UnorderedArraySet α) : Bool

O(1)

Equations

• Aesop.UnorderedArraySet.isEmpty s = Array.isEmpty s.rep

def Aesop.UnorderedArraySet.anyM {α : Type u_1} [BEq α] {m : Type → Type u_2} [Monad m] (p : α → m Bool) (s : Aesop.UnorderedArraySet α) (start : optParam Nat 0) (stop : optParam Nat (Aesop.UnorderedArraySet.size s)) : m Bool

O(n)

Equations

• Aesop.UnorderedArraySet.anyM p s start stop = Array.anyM p s.rep start stop

def Aesop.UnorderedArraySet.any {α : Type u_1} [BEq α] (p : α → Bool) (s : Aesop.UnorderedArraySet α) (start : optParam Nat 0) (stop : optParam Nat (Aesop.UnorderedArraySet.size s)) : Bool

O(n)

Equations

• Aesop.UnorderedArraySet.any p s start stop = Array.any s.rep p start stop

def Aesop.UnorderedArraySet.allM {α : Type u_1} [BEq α] {m : Type → Type u_2} [Monad m] (p : α → m Bool) (s : Aesop.UnorderedArraySet α) (start : optParam Nat 0) (stop : optParam Nat (Aesop.UnorderedArraySet.size s)) : m Bool

O(n)

Equations

• Aesop.UnorderedArraySet.allM p s start stop = Array.allM p s.rep start stop

def Aesop.UnorderedArraySet.all {α : Type u_1} [BEq α] (p : α → Bool) (s : Aesop.UnorderedArraySet α) (start : optParam Nat 0) (stop : optParam Nat (Aesop.UnorderedArraySet.size s)) : Bool

O(n)

Equations

• Aesop.UnorderedArraySet.all p s start stop = Array.all s.rep p start stop

instance Aesop.UnorderedArraySet.instBEqUnorderedArraySet {α : Type u_1} [BEq α] : BEq (Aesop.UnorderedArraySet α)

Equations

• Aesop.UnorderedArraySet.instBEqUnorderedArraySet = { beq := fun s t => Array.equalSet s.rep t.rep }

instance Aesop.UnorderedArraySet.instToStringUnorderedArraySet {α : Type u_1} [BEq α] [ToString α] : ToString (Aesop.UnorderedArraySet α)

Equations

• Aesop.UnorderedArraySet.instToStringUnorderedArraySet = { toString := fun s => toString s.rep }

instance Aesop.UnorderedArraySet.instToFormatUnorderedArraySet {α : Type u_1} [BEq α] [Lean.ToFormat α] : Lean.ToFormat (Aesop.UnorderedArraySet α)

Equations

• Aesop.UnorderedArraySet.instToFormatUnorderedArraySet = { format := fun s => Std.format s.rep }

instance Aesop.UnorderedArraySet.instToMessageDataUnorderedArraySet {α : Type} [BEq α] [Lean.ToMessageData α] : Lean.ToMessageData (Aesop.UnorderedArraySet α)

Equations

• Aesop.UnorderedArraySet.instToMessageDataUnorderedArraySet = { toMessageData := fun s => Lean.toMessageData s.rep }