Instances For
@[implicit_reducible]
O(1)
Instances For
@[implicit_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
@[implicit_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
@[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)
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
@[implicit_reducible]
@[implicit_reducible]
@[implicit_reducible]