The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Hi Coq-Club !

I face a case where the cofixpoint guard condition seems too strong to me. Here is a simplified version:

Require Import Streams.

CoInductive Tr :=
| L : nat -> Tr
| N : nat -> Tr -> Tr -> Tr.

CoFixpoint cfp (tr:Tr) (st:Stream nat) :=
  match tr with
    | L n => Cons n st
    | N n l r =>
      Cons n (cfp l (cfp r st))
  end.

How can I make this definition accepted by Coq?

Thank you all,
--
JH Jourdan