The Coq mailing list

[Venanzio Capretta <venanzio AT cs.ru.nl>]

In this specific case it is easy to separate the inductive and 
coinductive part by generalizing the first with respect to the second:

Inductive StrProg (Str: Set -> Type)(A:Set): Type :=
 darr : Str A -> StrProg Str A
| map : forall (B: Set), (B -> A) -> StrProg Str B -> StrProg Str A
| merge : (A -> A -> Ordering) ->
         StrProg Str A -> StrProg Str A -> StrProg Str A.

CoInductive Stream (A : Set) : Type :=
 cons : A -> StrProg Stream A -> Stream A.

It would be interesting to see if there is an example in which this 
trick doesn't work.

Venanzio



coq-club-request AT pauillac.inria.fr
 wrote:
> 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
>
>