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.
Prepend an element to a stream.
Instances For
n
-th element of a stream.
Instances For
Tail of a stream: Stream'.tail (h :: t) = t
.
Instances For
a ∈ s
means that a = Stream'.nth n s
for some n
.
The constant stream: Stream'.nth n (Stream'.const a) = a
.
Instances For
Iterates of a function as a stream.
Equations
- Stream'.iterate f a 0 = a
- Stream'.iterate f a (Nat.succ n) = f (Stream'.iterate f a n)
Instances For
Instances For
Instances For
Instances For
Elements of a stream with even indices.
Instances For
Elements of a stream with odd indices.
Instances For
take n s
returns a list of the n
first elements of stream s
Equations
- Stream'.take 0 x = []
- Stream'.take (Nat.succ n) x = Stream'.head x :: Stream'.take n (Stream'.tail x)
Instances For
An auxiliary definition for Stream'.cycle
corecursive def
Instances For
Tails of a stream, starting with Stream'.tail s
.
Instances For
An auxiliary definition for Stream'.inits
.
Instances For
A constant stream, same as Stream'.const
.
Instances For
The stream of natural numbers: Stream'.nth n Stream'.nats = n
.