stream

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

cons is basic list constructor.

ones: stream nat = cons one ones

Generics

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