{- Stream Run-Time Type:
   Copyright (c) Groupoid Infinity, 2014-2018. -}

module stream where
import nat

data stream (A: U) = cons (x: A) (xs: stream A)

tail (A: U): stream A -> stream A = split cons x xs -> xs
head (A: U): stream A -> A = split cons x xs -> x

fib (a b: nat)   : stream nat = cons a (fib b (add a b))
seq (start: nat) : stream nat = cons start (seq (succ start))

ones:  stream nat = cons one ones
zeros: stream nat = cons zero zeros
nats:  stream nat = seq zero