Equations
- Aesop.instInhabitedUnorderedArraySet = { default := { rep := default } }
Equations
- Aesop.UnorderedArraySet.instEmptyCollection = { emptyCollection := Aesop.UnorderedArraySet.empty }
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)
Equations
Instances For
Instances For
def
Aesop.UnorderedArraySet.ofPersistentHashSet
{α : Type u_1}
[BEq α]
[Hashable α]
(xs : Lean.PersistentHashSet α)
:
Equations
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)
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
- Aesop.UnorderedArraySet.instAppend = { append := Aesop.UnorderedArraySet.merge }
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
- Aesop.UnorderedArraySet.instForIn = { forIn := fun {β : Type ?u.30} [Monad m] (s : Aesop.UnorderedArraySet α) => forIn (Aesop.UnorderedArraySet.rep✝ s) }
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)
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)
Equations
Instances For
Equations
- Aesop.UnorderedArraySet.instToString = { toString := fun (s : Aesop.UnorderedArraySet α) => toString (Aesop.UnorderedArraySet.rep✝ s) }
Equations
- Aesop.UnorderedArraySet.instToFormat = { format := fun (s : Aesop.UnorderedArraySet α) => Std.format (Aesop.UnorderedArraySet.rep✝ s) }
Equations
- Aesop.UnorderedArraySet.instToMessageData = { toMessageData := fun (s : Aesop.UnorderedArraySet α) => Lean.toMessageData (Aesop.UnorderedArraySet.rep✝ s) }