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) : Type u

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

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

Prepend an element to a stream.

def Stream'.«term_::_» : Lean.TrailingParserDescr

Prepend an element to a stream.

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

Get the n-th element of a stream.

@[reducible, inline]

abbrev Stream'.head {α : Type u} (s : Stream' α) : α

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

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

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

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

Drop first n elements of a stream.

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

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

def Stream'.Any {α : Type u} (p : α → Prop) (s : Stream' α) : Prop

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

instance Stream'.instMembership {α : Type u} : Membership α (Stream' α)

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

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

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

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

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

def Stream'.enum {α : Type u} (s : Stream' α) : Stream' (ℕ × α)

Enumerate a stream by tagging each element with its index.

def Stream'.const {α : Type u} (a : α) : Stream' α

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

def Stream'.iterate {α : Type u} (f : α → α) (a : α) : Stream' α

Iterates of a function as a stream.

def Stream'.corec {α : Type u} {β : Type v} (f : α → β) (g : α → α) : α → Stream' β

Given functions f : α → β and g : α → α, corec f g creates a stream by:

1. Starting with an initial value a : α
2. Applying g repeatedly to get a stream of α values
3. Applying f to each value to convert them to β

def Stream'.corecOn {α : Type u} {β : Type v} (a : α) (f : α → β) (g : α → α) : Stream' β

Given an initial value a : α and functions f : α → β and g : α → α, corecOn a f g creates a stream by repeatedly:

1. Applying f to the current value to get the next stream element
2. Applying g to get the next value to process This is equivalent to corec f g a.

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

Given a function f : α → β × α, corec' f creates a stream by repeatedly:

1. Starting with an initial value a : α
2. Applying f to get both the next stream element (β) and next state value (α) This is a more convenient form when the next element and state are computed together.

def Stream'.corecState {σ α : Type u_1} (cmd : StateM σ α) (s : σ) : Stream' α

Use a state monad to generate a stream through corecursion

@[reducible, inline]

abbrev Stream'.unfolds {α : Type u} {β : Type v} (g : α → β) (f : α → α) (a : α) : Stream' β

def Stream'.interleave {α : Type u} (s₁ s₂ : Stream' α) : Stream' α

Interleave two streams.

def Stream'.«term_⋈_» : Lean.TrailingParserDescr

Interleave two streams.

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

Elements of a stream with even indices.

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

Elements of a stream with odd indices.

def Stream'.appendStream' {α : Type u} : List α → Stream' α → Stream' α

Append a stream to a list.

def Stream'.«term_++ₛ_» : Lean.TrailingParserDescr

Append a stream to a list.

def Stream'.take {α : Type u} : ℕ → Stream' α → List α

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

def Stream'.cycleF {α : Type u} : α × List α × α × List α → α

An auxiliary definition for Stream'.cycle corecursive def

def Stream'.cycleG {α : Type u} : α × List α × α × List α → α × List α × α × List α

An auxiliary definition for Stream'.cycle corecursive def

def Stream'.cycle {α : Type u} (l : List α) : l ≠ [] → Stream' α

Interpret a nonempty list as a cyclic stream.

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

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

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

An auxiliary definition for Stream'.inits.

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

Nonempty initial segments of a stream.

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

A constant stream, same as Stream'.const.

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

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

def Stream'.«term_⊛_» : Lean.TrailingParserDescr

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

def Stream'.nats : Stream' ℕ

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