# Definition of Stream' and functions on streams #

A stream Stream' α is an infinite sequence of elements of α. One can also think about it as an infinite list. In this file we define Stream' and some functions that take and/or return streams. Note that we already have Stream to represent a similar object, hence the awkward naming.

def Stream' (α : Type u) :

A stream Stream' α is an infinite sequence of elements of α.

Equations
Instances For
def Stream'.cons {α : Type u} (a : α) (s : ) :

Prepend an element to a stream.

Equations
Instances For
Equations
Instances For
def Stream'.get {α : Type u} (s : ) (n : ) :
α

Get the n-th element of a stream.

Equations
• s.get n = s n
Instances For
@[reducible, inline]
abbrev Stream'.head {α : Type u} (s : ) :
α

Head of a stream: Stream'.head s = Stream'.get s 0.

Equations
Instances For
def Stream'.tail {α : Type u} (s : ) :

Tail of a stream: Stream'.tail (h :: t) = t.

Equations
• s.tail i = s.get (i + 1)
Instances For
def Stream'.drop {α : Type u} (n : ) (s : ) :

Drop first n elements of a stream.

Equations
Instances For
def Stream'.All {α : Type u} (p : αProp) (s : ) :

Proposition saying that all elements of a stream satisfy a predicate.

Equations
• = ∀ (n : ), p (s.get n)
Instances For
def Stream'.Any {α : Type u} (p : αProp) (s : ) :

Proposition saying that at least one element of a stream satisfies a predicate.

Equations
• = ∃ (n : ), p (s.get n)
Instances For
instance Stream'.instMembership {α : Type u} :

a ∈ s means that a = Stream'.get n s for some n.

Equations
• Stream'.instMembership = { mem := fun (a : α) (s : ) => Stream'.Any (fun (b : α) => a = b) s }
def Stream'.map {α : Type u} {β : Type v} (f : αβ) (s : ) :

Apply a function f to all elements of a stream s.

Equations
Instances For
def Stream'.zip {α : Type u} {β : Type v} {δ : Type w} (f : αβδ) (s₁ : ) (s₂ : ) :

Zip two streams using a binary operation: Stream'.get n (Stream'.zip f s₁ s₂) = f (Stream'.get s₁) (Stream'.get s₂).

Equations
Instances For
def Stream'.enum {α : Type u} (s : ) :

Enumerate a stream by tagging each element with its index.

Equations
• s.enum n = (n, s.get n)
Instances For
def Stream'.const {α : Type u} (a : α) :

The constant stream: Stream'.get n (Stream'.const a) = a.

Equations
Instances For
def Stream'.iterate {α : Type u} (f : αα) (a : α) :

Iterates of a function as a stream.

Equations
Instances For
def Stream'.corec {α : Type u} {β : Type v} (f : αβ) (g : αα) :
α
Equations
Instances For
def Stream'.corecOn {α : Type u} {β : Type v} (a : α) (f : αβ) (g : αα) :
Equations
Instances For
def Stream'.corec' {α : Type u} {β : Type v} (f : αβ × α) :
α
Equations
Instances For
def Stream'.corecState {σ : Type u_1} {α : Type u_1} (cmd : StateM σ α) (s : σ) :

Use a state monad to generate a stream through corecursion

Equations
Instances For
@[reducible, inline]
abbrev Stream'.unfolds {α : Type u} {β : Type v} (g : αβ) (f : αα) (a : α) :
Equations
Instances For
def Stream'.interleave {α : Type u} (s₁ : ) (s₂ : ) :

Interleave two streams.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
def Stream'.even {α : Type u} (s : ) :

Elements of a stream with even indices.

Equations
• s.even = Stream'.corec (fun (s : ) => s.head) (fun (s : ) => s.tail.tail) s
Instances For
def Stream'.odd {α : Type u} (s : ) :

Elements of a stream with odd indices.

Equations
• s.odd = s.tail.even
Instances For
def Stream'.appendStream' {α : Type u} :
List α

Append a stream to a list.

Equations
Instances For
Equations
Instances For
def Stream'.take {α : Type u} :
List α

take n s returns a list of the n first elements of stream s

Equations
Instances For
def Stream'.cycleF {α : Type u} :
α × List α × α × List αα

An auxiliary definition for Stream'.cycle corecursive def

Equations
• = match x with | (v, fst, fst_1, snd) => v
Instances For
def Stream'.cycleG {α : Type u} :
α × List α × α × List αα × List α × α × List α

An auxiliary definition for Stream'.cycle corecursive def

Equations
• = match x with | (fst, [], v₀, l₀) => (v₀, l₀, v₀, l₀) | (fst, v₂ :: l₂, v₀, l₀) => (v₂, l₂, v₀, l₀)
Instances For
def Stream'.cycle {α : Type u} (l : List α) :
l []

Interpret a nonempty list as a cyclic stream.

Equations
• = match x✝, x with | [], h => absurd h | a :: l, x => Stream'.corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
Instances For
def Stream'.tails {α : Type u} (s : ) :

Tails of a stream, starting with Stream'.tail s.

Equations
Instances For
def Stream'.initsCore {α : Type u} (l : List α) (s : ) :

An auxiliary definition for Stream'.inits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Stream'.inits {α : Type u} (s : ) :

Nonempty initial segments of a stream.

Equations
Instances For
def Stream'.pure {α : Type u} (a : α) :

A constant stream, same as Stream'.const.

Equations
Instances For
def Stream'.apply {α : Type u} {β : Type v} (f : Stream' (αβ)) (s : ) :

Given a stream of functions and a stream of values, apply n-th function to n-th value.

Equations
• (f s) n = f.get n (s.get n)
Instances For
Equations
Instances For

The stream of natural numbers: Stream'.get n Stream'.nats = n.

Equations
Instances For