The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Corecursive calls aren't allowed to appear nested inside anything but 
constructors and [match]es.  Function application is never allowed, when 
reduction can't make it go away, which is the case here.  Sorry!

On 08/20/2014 11:31 AM, Jason Gross wrote:
> Why does Coq not notice that the following definition is manifestly 
> productive?
>
> Require Import Coq.Lists.Streams.
>
> Fixpoint stream_prepend_list {T} (ls : list T) (rest : Stream T) : 
> Stream T :=
>   match ls with
>     | nil => rest
>     | cons x xs => Cons x (stream_prepend_list xs rest)
>   end.
>
> CoFixpoint flatten_stream {T} (s : Stream (T * list T)) : Stream T :=
>   match s with
>     | Cons x xs => Cons (fst x) (stream_prepend_list (snd x) 
> (flatten_stream xs))
>   end.
>
> It seems that Coq doesn't want me to put anything between the 
> recursive call and the constructor, but it's syntactically obvious 
> that my definition is productive...