Documentation

Aesop.Util.UnorderedArraySet

structure Aesop.UnorderedArraySet (α : Type u_1) [BEq α] :

Type u_1

rep : Array α

instance Aesop.instInhabitedUnorderedArraySet {a✝ : Type u_1} {a✝¹ : BEq a✝} :

Inhabited (UnorderedArraySet a✝)

Equations

Aesop.instInhabitedUnorderedArraySet = { default := { rep := default } }

def Aesop.UnorderedArraySet.empty {α : Type u_1} [BEq α] :

UnorderedArraySet α

O(1)

Equations

Aesop.UnorderedArraySet.empty = { rep := #[] }

instance Aesop.UnorderedArraySet.instEmptyCollection {α : Type u_1} [BEq α] :

EmptyCollection (UnorderedArraySet α)

Equations

Aesop.UnorderedArraySet.instEmptyCollection = { emptyCollection := Aesop.UnorderedArraySet.empty }

def Aesop.UnorderedArraySet.singleton {α : Type u_1} [BEq α] (a : α) :

UnorderedArraySet α

O(1)

Equations

Aesop.UnorderedArraySet.singleton a = { rep := #[a] }

def Aesop.UnorderedArraySet.insert {α : Type u_1} [BEq α] (x : α) :

UnorderedArraySet α → UnorderedArraySet α

O(n)

Equations

Aesop.UnorderedArraySet.insert x { rep := rep } = if rep.contains x = true then { rep := rep } else { rep := rep.push x }

def Aesop.UnorderedArraySet.ofDeduplicatedArray {α : Type u_1} [BEq α] (xs : Array α) :

UnorderedArraySet α

Precondition: xs contains no duplicates.

Equations

Aesop.UnorderedArraySet.ofDeduplicatedArray xs = { rep := xs }

def Aesop.UnorderedArraySet.ofSortedArray {α : Type u_1} [BEq α] (xs : Array α) :

UnorderedArraySet α

Precondition: xs is sorted.

Equations

Aesop.UnorderedArraySet.ofSortedArray xs = { rep := xs.dedupSorted }

def Aesop.UnorderedArraySet.ofArray {α : Type u_1} [BEq α] [ord : Ord α] (xs : Array α) :

UnorderedArraySet α

O(n*log(n))

Equations

Aesop.UnorderedArraySet.ofArray xs = { rep := xs.sortDedup }

def Aesop.UnorderedArraySet.ofArraySlow {α : Type u_1} [BEq α] (xs : Array α) :

UnorderedArraySet α

O(n^2)

Equations

Aesop.UnorderedArraySet.ofArraySlow xs = Array.foldl (fun (s : Aesop.UnorderedArraySet α) (x : α) => Aesop.UnorderedArraySet.insert x s) ∅ xs

def Aesop.UnorderedArraySet.ofHashSet {α : Type u_1} [BEq α] [Hashable α] (xs : Std.HashSet α) :

UnorderedArraySet α

Equations

Aesop.UnorderedArraySet.ofHashSet xs = { rep := xs.toArray }

def Aesop.UnorderedArraySet.ofPersistentHashSet {α : Type u_1} [BEq α] [Hashable α] (xs : Lean.PersistentHashSet α) :

UnorderedArraySet α

Equations

Aesop.UnorderedArraySet.ofPersistentHashSet xs = { rep := Lean.PersistentHashSet.fold (fun (as : Array α) (a : α) => as.push a) #[] xs }

def Aesop.UnorderedArraySet.toArray {α : Type u_1} [BEq α] (s : UnorderedArraySet α) :

Equations

s.toArray = Aesop.UnorderedArraySet.rep✝ s

def Aesop.UnorderedArraySet.erase {α : Type u_1} [BEq α] (x : α) (s : UnorderedArraySet α) :

UnorderedArraySet α

O(n)

Equations

Aesop.UnorderedArraySet.erase x s = { rep := (Aesop.UnorderedArraySet.rep✝ s).erase x }

def Aesop.UnorderedArraySet.filterM {α : Type} [BEq α] {m : Type → Type u_1} [Monad m] (p : α → m Bool) (s : UnorderedArraySet α) :

m (UnorderedArraySet α)

O(n)

Equations

Aesop.UnorderedArraySet.filterM p s = do let __do_lift ← Array.filterM p (Aesop.UnorderedArraySet.rep✝ s) pure { rep := __do_lift }

def Aesop.UnorderedArraySet.filter {α : Type u_1} [BEq α] (p : α → Bool) (s : UnorderedArraySet α) :

UnorderedArraySet α

O(n)

Equations

Aesop.UnorderedArraySet.filter p s = { rep := Array.filter p (Aesop.UnorderedArraySet.rep✝ s) }

def Aesop.UnorderedArraySet.merge {α : Type u_1} [BEq α] (s t : UnorderedArraySet α) :

UnorderedArraySet α

O(n*m)

Equations

s.merge t = { rep := (Aesop.UnorderedArraySet.rep✝ s).mergeUnsortedDedup (Aesop.UnorderedArraySet.rep✝ t) }

instance Aesop.UnorderedArraySet.instAppend {α : Type u_1} [BEq α] :

Append (UnorderedArraySet α)

Equations

Aesop.UnorderedArraySet.instAppend = { append := Aesop.UnorderedArraySet.merge }

def Aesop.UnorderedArraySet.contains {α : Type u_1} [BEq α] (x : α) (s : UnorderedArraySet α) :

O(n)

Equations

Aesop.UnorderedArraySet.contains x s = (Aesop.UnorderedArraySet.rep✝ s).contains x

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

Aesop.UnorderedArraySet.foldM f init s = Array.foldlM f init (Aesop.UnorderedArraySet.rep✝ s)

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

Aesop.UnorderedArraySet.fold f init s = Array.foldl f init (Aesop.UnorderedArraySet.rep✝ s)

def Aesop.UnorderedArraySet.partition {α : Type u_1} [BEq α] (f : α → Bool) (s : UnorderedArraySet α) :

UnorderedArraySet α × UnorderedArraySet α

Equations

Aesop.UnorderedArraySet.partition f s = match Array.partition f (Aesop.UnorderedArraySet.rep✝ s) with | (xs, ys) => ({ rep := xs }, { rep := ys })

def Aesop.UnorderedArraySet.size {α : Type u_1} [BEq α] (s : UnorderedArraySet α) :

O(1)

Equations

s.size = (Aesop.UnorderedArraySet.rep✝ s).size

def Aesop.UnorderedArraySet.isEmpty {α : Type u_1} [BEq α] (s : UnorderedArraySet α) :

O(1)

Equations

s.isEmpty = (Aesop.UnorderedArraySet.rep✝ s).isEmpty

def Aesop.UnorderedArraySet.anyM {α : Type u_1} [BEq α] {m : Type → Type u_2} [Monad m] (p : α → m Bool) (s : UnorderedArraySet α) (start : Nat := 0) (stop : Nat := s.size) :

O(n)

Equations

Aesop.UnorderedArraySet.anyM p s start stop = Array.anyM p (Aesop.UnorderedArraySet.rep✝ s) start stop

def Aesop.UnorderedArraySet.any {α : Type u_1} [BEq α] (p : α → Bool) (s : UnorderedArraySet α) (start : Nat := 0) (stop : Nat := s.size) :

O(n)

Equations

Aesop.UnorderedArraySet.any p s start stop = (Aesop.UnorderedArraySet.rep✝ s).any p start stop

def Aesop.UnorderedArraySet.allM {α : Type u_1} [BEq α] {m : Type → Type u_2} [Monad m] (p : α → m Bool) (s : UnorderedArraySet α) (start : Nat := 0) (stop : Nat := s.size) :

O(n)

Equations

Aesop.UnorderedArraySet.allM p s start stop = Array.allM p (Aesop.UnorderedArraySet.rep✝ s) start stop

def Aesop.UnorderedArraySet.all {α : Type u_1} [BEq α] (p : α → Bool) (s : UnorderedArraySet α) (start : Nat := 0) (stop : Nat := s.size) :

O(n)

Equations

Aesop.UnorderedArraySet.all p s start stop = (Aesop.UnorderedArraySet.rep✝ s).all p start stop

instance Aesop.UnorderedArraySet.instToString {α : Type u_1} [BEq α] [ToString α] :

ToString (UnorderedArraySet α)

Equations

Aesop.UnorderedArraySet.instToString = { toString := fun (s : Aesop.UnorderedArraySet α) => toString (Aesop.UnorderedArraySet.rep✝ s) }

instance Aesop.UnorderedArraySet.instToFormat {α : Type u_1} [BEq α] [Std.ToFormat α] :

Std.ToFormat (UnorderedArraySet α)

Equations

Aesop.UnorderedArraySet.instToFormat = { format := fun (s : Aesop.UnorderedArraySet α) => Std.format (Aesop.UnorderedArraySet.rep✝ s) }

instance Aesop.UnorderedArraySet.instToMessageData {α : Type} [BEq α] [Lean.ToMessageData α] :

Lean.ToMessageData (UnorderedArraySet α)

Equations

Aesop.UnorderedArraySet.instToMessageData = { toMessageData := fun (s : Aesop.UnorderedArraySet α) => Lean.toMessageData (Aesop.UnorderedArraySet.rep✝ s) }