The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

Hi,

This is related to my previous question, but a lot simpler (hopefully I didn't simplify the problem too much). I don't understand how to 
mix induction and coinduction in Coq. Here is a *very* simple example:

Require Import List.

CoInductive T : Set :=
  | A : T -> T 
  | B : list T -> T.

CoFixpoint f (t : T) : T :=
  match t with
  | A t1' => A (f t1')
  | B t1s => B (map f t1s)
  end.

This definition of [f] seems ok to me, but is rejected as not guarded because the recursive argument appears as argument to a function (in this case, map). How should one define functions and data types like this? (I don't care if I have to redefine list; I'm only using list as an example -- the loss of the use of library functions is not an issue.) 

Thanks,

Edsko

PS. I seem to recall that a question like this came up before, but I can't find it.