The Coq mailing list

["Jim Apple" <coq-club AT jbapple.com>]

Is it possible to write a pair of mutually recursive types of which
one is inductive and the other coinductive, as in:

http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=109

Jim

P.S.

I haven't tried the other two techniques listed (Conor McBride's and
"A Unifying Approach to Recursive and Co-recursive Definitions"s), but
here's the Haskell code I'm trying to translate:

data Stream a = Stream a (Stream a) (Stream a) deriving (Show)

instance Functor Stream where
    fmap f (Stream x od ev) = Stream (f x) (fmap f od) (fmap f ev)

oddFromEven f x ~(Stream h od ev) =
    Stream x (oddFromEven f (f h) ev) (fmap f od)

iterateS :: (a -> a) -> a -> Stream a
iterateS f x =
    let ev = fmap f od
        od = oddFromEven f (f x) ev
    in
      Stream x od ev