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
Prepend an element to a stream.
Equations
- Stream'.«term_::_» = Lean.ParserDescr.trailingNode `Stream'.«term_::_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :: ") (Lean.ParserDescr.cat `term 67))
Instances For
Drop first n
elements of a stream.
Instances For
Proposition saying that all elements of a stream satisfy a predicate.
Equations
- Stream'.All p s = ∀ (n : ℕ), p (s.get n)
Instances For
a ∈ s
means that a = Stream'.get n s
for some n
.
Equations
- Stream'.instMembership = { mem := fun (s : Stream' α) (a : α) => Stream'.Any (fun (b : α) => a = b) s }
Apply a function f
to all elements of a stream s
.
Equations
Instances For
The constant stream: Stream'.get n (Stream'.const a) = a
.
Instances For
Iterates of a function as a stream.
Instances For
Instances For
Instances For
Instances For
Use a state monad to generate a stream through corecursion
Equations
Instances For
Instances For
Interleave two streams.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Interleave two streams.
Equations
- Stream'.«term_⋈_» = Lean.ParserDescr.trailingNode `Stream'.«term_⋈_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋈ ") (Lean.ParserDescr.cat `term 66))
Instances For
Elements of a stream with even indices.
Equations
- s.even = Stream'.corec Stream'.head (fun (s : Stream' α) => s.tail.tail) s
Instances For
Append a stream to a list.
Equations
- Stream'.«term_++ₛ_» = Lean.ParserDescr.trailingNode `Stream'.«term_++ₛ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ++ₛ ") (Lean.ParserDescr.cat `term 66))
Instances For
take n s
returns a list of the n
first elements of stream s
Instances For
An auxiliary definition for Stream'.cycle
corecursive def
Instances For
Interpret a nonempty list as a cyclic stream.
Equations
Instances For
An auxiliary definition for Stream'.inits
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A constant stream, same as Stream'.const
.
Instances For
Given a stream of functions and a stream of values, apply n
-th function to n
-th value.
Equations
- Stream'.«term_⊛_» = Lean.ParserDescr.trailingNode `Stream'.«term_⊛_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊛ ") (Lean.ParserDescr.cat `term 76))
Instances For
The stream of natural numbers: Stream'.get n Stream'.nats = n
.