# 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