stream.is_seq

A stream s : option α is a sequence if s.nth n = none implies s.nth (n + 1) = none.

seq

seq α is the type of possibly infinite lists (referred here as sequences). It is encoded as an infinite stream of options such that if f n = none, then f m = none for all m ≥ n.

seq1

seq1 α is the type of nonempty sequences.

seq.nil

The empty sequence

seq.cons

Prepend an element to a sequence

seq.nth

Get the nth element of a sequence (if it exists)

seq.terminated_at

A sequence has terminated at position n if the value at position n equals none.

seq.terminated_at_decidable

It is decidable whether a sequence terminates at a given position.

seq.terminates

A sequence terminates if there is some position n at which it has terminated.

seq.omap

Functorial action of the functor option (α × _)

seq.head

Get the first element of a sequence

seq.tail

Get the tail of a sequence (or nil if the sequence is nil)

seq.terminated_stable

If a sequence terminated at position n, it also terminated at m ≥ n .

seq.ge_stable

If s.nth n = some aₙ for some value aₙ, then there is also some value aₘ such that s.nth = some aₘ for m ≤ n.

seq.destruct

Destructor for a sequence, resulting in either none (for nil) or some (a, s) (for cons a s).

seq.corec

Corecursor for seq α as a coinductive type. Iterates f to produce new elements of the sequence until none is obtained.

seq.of_list

Embed a list as a sequence

seq.of_stream

Embed an infinite stream as a sequence

seq.of_lazy_list

Embed a lazy_list α as a sequence. Note that even though this is non-meta, it will produce infinite sequences if used with cyclic lazy_lists created by meta constructions.

seq.to_lazy_list

Translate a sequence into a lazy_list. Since lazy_list and list are isomorphic as non-meta types, this function is necessarily meta.

seq.force_to_list

Translate a sequence to a list. This function will run forever if run on an infinite sequence.

seq.nats

The sequence of natural numbers some 0, some 1, ...

seq.append

Append two sequences. If s₁ is infinite, then s₁ ++ s₂ = s₁, otherwise it puts s₂ at the location of the nil in s₁.

seq.map

Map a function over a sequence.

seq.join

Flatten a sequence of sequences. (It is required that the sequences be nonempty to ensure productivity; in the case of an infinite sequence of nil, the first element is never generated.)

seq.drop

Remove the first n elements from the sequence.

seq.take

Take the first n elements of the sequence (producing a list)

seq.split_at

Split a sequence at n, producing a finite initial segment and an infinite tail.

seq.zip_with

Combine two sequences with a function

seq.zip

Pair two sequences into a sequence of pairs

seq.unzip

Separate a sequence of pairs into two sequences

seq.to_list

Convert a sequence which is known to terminate into a list

seq.to_stream

Convert a sequence which is known not to terminate into a stream

seq.to_list_or_stream

Convert a sequence into either a list or a stream depending on whether it is finite or infinite. (Without decidability of the infiniteness predicate, this is not constructively possible.)

seq.to_list'

Convert a sequence into a list, embedded in a computation to allow for the possibility of infinite sequences (in which case the computation never returns anything).

seq1.to_seq

Convert a seq1 to a sequence.

seq1.map

Map a function on a seq1

seq1.join

Flatten a nonempty sequence of nonempty sequences

seq1.ret

The return operator for the seq1 monad, which produces a singleton sequence.

seq1.bind

The bind operator for the seq1 monad, which maps f on each element of s and appends the results together. (Not all of s may be evaluated, because the first few elements of s may already produce an infinite result.)