The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

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.

(* Error:

Recursive definition of flatten_stream is ill-formed.

In environment

flatten_stream : forall T : Type, Stream (T * list T) -> Stream T

T : Type

s : Stream (T * list T)

x : T * list T

xs : Stream (T * list T)

Sub-_expression_ "stream_prepend_list (snd x) (flatten_stream T xs)" not in

guarded form (should be a constructor, an abstraction, a match, a cofix or a

recursive call).

Recursive definition is:

"fun (T : Type) (s : Stream (T * list T)) =>

 match s with

 | Cons x xs =>

     Cons (fst x) (stream_prepend_list (snd x) (flatten_stream T 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...

-Jason