Miscellaneous definitions concerning weak sequences

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

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

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

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.

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

Replace the nth element of s with a.

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

Remove the nth element of s.

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.

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

Select the elements of s that satisfy p.

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

Get the first element of s satisfying p.

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

Zip a function over two weak sequences

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

Zip two weak sequences into a single sequence of pairs

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

Get the list of indexes of elements of s satisfying p

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

Get the index of the first element of s satisfying p

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

Get the index of the first occurrence of a in s

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

Get the indexes of occurrences of a in s

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).

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

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

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

Calculate one step of computation

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

Get the first n elements of a weak sequence

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

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

Returns true if any element of s satisfies p

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

Returns true if every element of s satisfies p

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.)

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

Get the weak sequence of initial segments of the input sequence

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

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