@[instance_reducible]
O(1)
Instances For
@[instance_reducible]
O(1)
Instances For
Precondition: xs contains no duplicates.
Instances For
Precondition: xs is sorted.
Instances For
O(n*log(n))
Instances For
O(n^2)
Instances For
Instances For
def Aesop.UnorderedArraySet.ofPersistentHashSet {α : Type u_1} [BEq α] [Hashable α] (xs : Lean.PersistentHashSet α) :
Instances For
Instances For
O(n)
Instances For
def Aesop.UnorderedArraySet.filterM {α : Type} [BEq α] {m : Type → Type u_1} [Monad m] (p : α → m Bool) (s : UnorderedArraySet α) :
m (UnorderedArraySet α)
O(n)
Instances For
def Aesop.UnorderedArraySet.filter {α : Type u_1} [BEq α] (p : α → Bool) (s : UnorderedArraySet α) :
O(n)
Instances For
O(n*m)
Instances For
@[instance_reducible]
O(n)
Instances For
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)
Instances For
@[instance_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)
Instances For
def Aesop.UnorderedArraySet.partition {α : Type u_1} [BEq α] (f : α → Bool) (s : UnorderedArraySet α) :
Instances For
O(1)
Instances For
O(1)
Instances For
def Aesop.UnorderedArraySet.any {α : Type u_1} [BEq α] (p : α → Bool) (s : UnorderedArraySet α) (start : Nat := 0) (stop : Nat := s.size) :
O(n)
Instances For
def Aesop.UnorderedArraySet.all {α : Type u_1} [BEq α] (p : α → Bool) (s : UnorderedArraySet α) (start : Nat := 0) (stop : Nat := s.size) :
O(n)
Instances For
@[instance_reducible]
@[instance_reducible]
@[instance_reducible]