instance
Aesop.instInhabitedUnorderedArraySet :
{a : Type u_1} → {a_1 : BEq a} → Inhabited (Aesop.UnorderedArraySet a)
Equations
- Aesop.instInhabitedUnorderedArraySet = { default := { rep := default } }
Equations
- Aesop.UnorderedArraySet.instEmptyCollection = { emptyCollection := Aesop.UnorderedArraySet.empty }
O(n)
Equations
- Aesop.UnorderedArraySet.insert x✝ x = match x with | { rep := rep } => if rep.contains x✝ = true then { rep := rep } else { rep := rep.push x✝ }
Instances For
Precondition: xs
contains no duplicates.
Equations
- Aesop.UnorderedArraySet.ofDeduplicatedArray xs = { rep := xs }
Instances For
Precondition: xs
is sorted.
Equations
- Aesop.UnorderedArraySet.ofSortedArray xs = { rep := xs.dedupSorted }
Instances For
def
Aesop.UnorderedArraySet.ofArray
{α : Type u_1}
[BEq α]
[ord : Ord α]
[Inhabited α]
(xs : Array α)
:
O(n*log(n))
Equations
- Aesop.UnorderedArraySet.ofArray xs = { rep := xs.sortDedup }
Instances For
O(n^2)
Equations
- Aesop.UnorderedArraySet.ofArraySlow xs = Array.foldl (fun (s : Aesop.UnorderedArraySet α) (x : α) => Aesop.UnorderedArraySet.insert x s) ∅ xs 0
Instances For
Equations
- Aesop.UnorderedArraySet.ofHashSet xs = { rep := xs.toArray }
Instances For
def
Aesop.UnorderedArraySet.ofPersistentHashSet
{α : Type u_1}
[BEq α]
[Hashable α]
(xs : Lean.PersistentHashSet α)
:
Equations
- Aesop.UnorderedArraySet.ofPersistentHashSet xs = { rep := Lean.PersistentHashSet.fold (fun (as : Array α) (a : α) => as.push a) #[] xs }
Instances For
Equations
- s.toArray = s.rep
Instances For
O(n)
Equations
- Aesop.UnorderedArraySet.erase x s = { rep := s.rep.erase x }
Instances For
def
Aesop.UnorderedArraySet.filterM
{α : Type}
[BEq α]
{m : Type → Type u_1}
[Monad m]
(p : α → m Bool)
(s : Aesop.UnorderedArraySet α)
:
m (Aesop.UnorderedArraySet α)
O(n)
Equations
- Aesop.UnorderedArraySet.filterM p s = do let __do_lift ← Array.filterM p s.rep 0 pure { rep := __do_lift }
Instances For
def
Aesop.UnorderedArraySet.filter
{α : Type u_1}
[BEq α]
(p : α → Bool)
(s : Aesop.UnorderedArraySet α)
:
O(n)
Equations
- Aesop.UnorderedArraySet.filter p s = { rep := Array.filter p s.rep 0 }
Instances For
def
Aesop.UnorderedArraySet.merge
{α : Type u_1}
[BEq α]
(s : Aesop.UnorderedArraySet α)
(t : Aesop.UnorderedArraySet α)
:
O(n*m)
Equations
- s.merge t = { rep := s.rep.mergeUnsortedDedup t.rep }
Instances For
Equations
- Aesop.UnorderedArraySet.instAppend = { append := Aesop.UnorderedArraySet.merge }
def
Aesop.UnorderedArraySet.contains
{α : Type u_1}
[BEq α]
(x : α)
(s : Aesop.UnorderedArraySet α)
:
O(n)
Equations
- Aesop.UnorderedArraySet.contains x s = s.rep.contains x
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 : Aesop.UnorderedArraySet α)
:
m σ
O(n)
Equations
- Aesop.UnorderedArraySet.foldM f init s = Array.foldlM f init s.rep 0
Instances For
instance
Aesop.UnorderedArraySet.instForInOfMonad
{α : Type u_1}
[BEq α]
{m : Type u_2 → Type u_3}
[Monad m]
:
ForIn m (Aesop.UnorderedArraySet α) α
Equations
- Aesop.UnorderedArraySet.instForInOfMonad = { forIn := fun {β : Type u_2} [Monad m] (s : Aesop.UnorderedArraySet α) => s.rep.forIn }
def
Aesop.UnorderedArraySet.fold
{α : Type u_1}
[BEq α]
{σ : Type u_2}
(f : σ → α → σ)
(init : σ)
(s : Aesop.UnorderedArraySet α)
:
σ
O(n)
Equations
- Aesop.UnorderedArraySet.fold f init s = Array.foldl f init s.rep 0
Instances For
def
Aesop.UnorderedArraySet.partition
{α : Type u_1}
[BEq α]
(f : α → Bool)
(s : Aesop.UnorderedArraySet α)
:
Equations
- Aesop.UnorderedArraySet.partition f s = match Array.partition f s.rep with | (xs, ys) => ({ rep := xs }, { rep := ys })
Instances For
def
Aesop.UnorderedArraySet.anyM
{α : Type u_1}
[BEq α]
{m : Type → Type u_2}
[Monad m]
(p : α → m Bool)
(s : Aesop.UnorderedArraySet α)
(start : optParam Nat 0)
(stop : optParam Nat s.size)
:
m Bool
O(n)
Equations
- Aesop.UnorderedArraySet.anyM p s start stop = Array.anyM p s.rep start stop
Instances For
def
Aesop.UnorderedArraySet.any
{α : Type u_1}
[BEq α]
(p : α → Bool)
(s : Aesop.UnorderedArraySet α)
(start : optParam Nat 0)
(stop : optParam Nat s.size)
:
O(n)
Equations
- Aesop.UnorderedArraySet.any p s start stop = s.rep.any p start stop
Instances For
def
Aesop.UnorderedArraySet.allM
{α : Type u_1}
[BEq α]
{m : Type → Type u_2}
[Monad m]
(p : α → m Bool)
(s : Aesop.UnorderedArraySet α)
(start : optParam Nat 0)
(stop : optParam Nat s.size)
:
m Bool
O(n)
Equations
- Aesop.UnorderedArraySet.allM p s start stop = Array.allM p s.rep start stop
Instances For
def
Aesop.UnorderedArraySet.all
{α : Type u_1}
[BEq α]
(p : α → Bool)
(s : Aesop.UnorderedArraySet α)
(start : optParam Nat 0)
(stop : optParam Nat s.size)
:
O(n)
Equations
- Aesop.UnorderedArraySet.all p s start stop = s.rep.all p start stop
Instances For
Equations
- Aesop.UnorderedArraySet.instBEq = { beq := fun (s t : Aesop.UnorderedArraySet α) => s.rep.equalSet t.rep }
Equations
- Aesop.UnorderedArraySet.instToString = { toString := fun (s : Aesop.UnorderedArraySet α) => toString s.rep }
Equations
- Aesop.UnorderedArraySet.instToFormat = { format := fun (s : Aesop.UnorderedArraySet α) => Std.format s.rep }
Equations
- Aesop.UnorderedArraySet.instToMessageData = { toMessageData := fun (s : Aesop.UnorderedArraySet α) => Lean.toMessageData s.rep }