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