The Coq mailing list

[Jean-Baptiste Jeannin <jeannin AT cs.cornell.edu>]

Hi,

I am trying to define a type with both inductive constructors and coinductive constructors (really destructors).

With the [Inductive] keyword, I can define a type with all constructors inductive, as in:

Inductive list: Type:=

  | LNil : list

  | LCons : nat -> list -> list.

and similarly with the [CoInductive] keyword, I can define a type with all constructors coinductive, as in:

CoInductive stream : Type :=

  | SCons : nat -> stream -> stream.

If I want some constructors to be inductive and others to be coinductive, an idea I had was to use two mutually recursive types, with a construct akin to:

CoInductive even_list : Set :=

| ENil : even_list

| ECons : nat -> odd_list -> even_list

with odd_list : Set :=

| OCons : nat -> even_list -> odd_list.

But I can't seem to make odd_list just [Inductive], while keeping even_list [CoInductive]. Is there any way I could do this? Or any other way to mix Inductive and CoInductive constructors?

(examples taken or inspired from http://adam.chlipala.net/cpdt/html/Coinductive.html and http://adam.chlipala.net/cpdt/html/InductiveTypes.html)

Thank you,

Jean-Baptiste