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

• rep : Array α

@[implicit_reducible]

instance Aesop.instInhabitedUnorderedArraySet {a✝ : Type u_1} {a✝¹ : BEq a✝} : Inhabited (UnorderedArraySet a✝)

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

O(1)

@[implicit_reducible]

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

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

O(1)

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

O(n)

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

Precondition: xs contains no duplicates.

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

Precondition: xs is sorted.

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

O(n*log(n))

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

O(n^2)

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

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

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

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

O(n)

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

O(n)

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

O(n)

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

O(n*m)

@[implicit_reducible]

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

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

O(n)

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

O(n)

@[implicit_reducible]

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

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

O(n)

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

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

O(1)

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

O(1)

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

O(n)

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

O(n)

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

O(n)

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

O(n)

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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