Stream package contains inductive data type definition representing infinite parametrized homogenous lists, its generic functions, theorems and examples of usage.

data stream (A: U) = cons (a: A) (as: stream A)


cons is basic list constructor.

ones: stream nat = cons one ones


head (A : U) : stream A -> A

Returns a first element of an infinite stream.

tail (A : U) : stream A -> stream A

Returns tail of an infinite stream.

> let a: nat = head nat (tail nat ones) in a
EVAL: suc zero