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