Miscellaneous definitions concerning weak sequences

These definitions, as well as those in Mathlib.Data.WSeq.Productive, are not needed for the development of Mathlib.Data.Seq.Parallel.

def Stream'.WSeq.length {α : Type u} (s : WSeq α) : Computation ℕ

Get the length of s (if it is finite and completes in finite time).

Equations

• One or more equations did not get rendered due to their size.

class Stream'.WSeq.IsFinite {α : Type u} (s : WSeq α) : Prop

A weak sequence is finite if toList s terminates. Equivalently, it is a finite number of think and cons applied to nil.

• out : s.toList.Terminates

instance Stream'.WSeq.toList_terminates {α : Type u} (s : WSeq α) [h : s.IsFinite] : s.toList.Terminates

def Stream'.WSeq.get {α : Type u} (s : WSeq α) [s.IsFinite] : List α

Get the list corresponding to a finite weak sequence.

Equations

• s.get = s.toList.get

def Stream'.WSeq.updateNth {α : Type u} (s : WSeq α) (n : ℕ) (a : α) : WSeq α

Replace the nth element of s with a.

Equations

• One or more equations did not get rendered due to their size.

def Stream'.WSeq.removeNth {α : Type u} (s : WSeq α) (n : ℕ) : WSeq α

Remove the nth element of s.

Equations

• One or more equations did not get rendered due to their size.

def Stream'.WSeq.filterMap {α : Type u} {β : Type v} (f : α → Option β) : WSeq α → WSeq β

Map the elements of s over f, removing any values that yield none.

Equations

• One or more equations did not get rendered due to their size.

def Stream'.WSeq.filter {α : Type u} (p : α → Prop) [DecidablePred p] : WSeq α → WSeq α

Select the elements of s that satisfy p.

Equations

• Stream'.WSeq.filter p = Stream'.WSeq.filterMap fun (a : α) => if p a then some a else none

def Stream'.WSeq.find {α : Type u} (p : α → Prop) [DecidablePred p] (s : WSeq α) : Computation (Option α)

Get the first element of s satisfying p.

Equations

• Stream'.WSeq.find p s = (Stream'.WSeq.filter p s).head

def Stream'.WSeq.zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (s1 : WSeq α) (s2 : WSeq β) : WSeq γ

Zip a function over two weak sequences

Equations

• One or more equations did not get rendered due to their size.

def Stream'.WSeq.zip {α : Type u} {β : Type v} : WSeq α → WSeq β → WSeq (α × β)

Zip two weak sequences into a single sequence of pairs

Equations

• Stream'.WSeq.zip = Stream'.WSeq.zipWith Prod.mk

def Stream'.WSeq.findIndexes {α : Type u} (p : α → Prop) [DecidablePred p] (s : WSeq α) : WSeq ℕ

Get the list of indexes of elements of s satisfying p

Equations

• Stream'.WSeq.findIndexes p s = Stream'.WSeq.filterMap (fun (x : α × ℕ) => match x with | (a, n) => if p a then some n else none) (s.zip ↑Stream'.nats)

def Stream'.WSeq.findIndex {α : Type u} (p : α → Prop) [DecidablePred p] (s : WSeq α) : Computation ℕ

Get the index of the first element of s satisfying p

Equations

• Stream'.WSeq.findIndex p s = (fun (o : Option ℕ) => o.getD 0) <$> (Stream'.WSeq.findIndexes p s).head

def Stream'.WSeq.indexOf {α : Type u} [DecidableEq α] (a : α) : WSeq α → Computation ℕ

Get the index of the first occurrence of a in s

Equations

• Stream'.WSeq.indexOf a = Stream'.WSeq.findIndex (Eq a)

def Stream'.WSeq.indexesOf {α : Type u} [DecidableEq α] (a : α) : WSeq α → WSeq ℕ

Get the indexes of occurrences of a in s

Equations

• Stream'.WSeq.indexesOf a = Stream'.WSeq.findIndexes (Eq a)

def Stream'.WSeq.union {α : Type u} (s1 s2 : WSeq α) : WSeq α

union s1 s2 is a weak sequence which interleaves s1 and s2 in some order (nondeterministically).

Equations

• One or more equations did not get rendered due to their size.

def Stream'.WSeq.isEmpty {α : Type u} (s : WSeq α) : Computation Bool

Returns true if s is nil and false if s has an element

Equations

• s.isEmpty = Computation.map Option.isNone s.head

def Stream'.WSeq.compute {α : Type u} (s : WSeq α) : WSeq α

Calculate one step of computation

Equations

• s.compute = match Stream'.Seq.destruct s with | some (none, s') => s' | x => s

def Stream'.WSeq.take {α : Type u} (s : WSeq α) (n : ℕ) : WSeq α

Get the first n elements of a weak sequence

Equations

• One or more equations did not get rendered due to their size.

def Stream'.WSeq.splitAt {α : Type u} (s : WSeq α) (n : ℕ) : Computation (List α × WSeq α)

Split the sequence at position n into a finite initial segment and the weak sequence tail

Equations

• One or more equations did not get rendered due to their size.

def Stream'.WSeq.any {α : Type u} (s : WSeq α) (p : α → Bool) : Computation Bool

Returns true if any element of s satisfies p

Equations

• One or more equations did not get rendered due to their size.

def Stream'.WSeq.all {α : Type u} (s : WSeq α) (p : α → Bool) : Computation Bool

Returns true if every element of s satisfies p

Equations

• One or more equations did not get rendered due to their size.

def Stream'.WSeq.scanl {α : Type u} {β : Type v} (f : α → β → α) (a : α) (s : WSeq β) : WSeq α

Apply a function to the elements of the sequence to produce a sequence of partial results. (There is no scanr because this would require working from the end of the sequence, which may not exist.)

Equations

• One or more equations did not get rendered due to their size.

def Stream'.WSeq.inits {α : Type u} (s : WSeq α) : WSeq (List α)

Get the weak sequence of initial segments of the input sequence

Equations

• One or more equations did not get rendered due to their size.

def Stream'.WSeq.collect {α : Type u} (s : WSeq α) (n : ℕ) : List α

Like take, but does not wait for a result. Calculates n steps of computation and returns the sequence computed so far

Equations

• s.collect n = List.filterMap id (Stream'.Seq.take n s)

theorem Stream'.WSeq.length_eq_map {α : Type u} (s : WSeq α) : s.length = Computation.map List.length s.toList