streams.agda

{-# OPTIONS  --copatterns #-}
module streams where

record Stream (A : Set) : Set where
    coinductive
    field
        hd : A
        tl : Stream A

open Stream

data Foo : Set where
    A B : Foo

Foos : Foo -> Stream Foo
hd (Foos A) = B
hd (Foos B) = A
tl (Foos f) = Foos f