The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Edsko de Vries wrote:
> Example: suppose we define coinductive trees as
>
> CoInductive cotree : Set :=
> | coleaf : cotree
> | cobranch : cotree -> cotree -> cotree.
>
> Consider a function to count the number of leaves in a tree
>
> leaves : cotree -> conat
>
> (the domain is conat because there might be infinitely many leaves). 
> This function is "obviously not productive": there are infinitely 
> large trees that don't have any leaves but simply keep on branching 
> forever.

Since you haven't defined [conat], it's not clear to me that you can't 
write this function. A reasonable definition of [conat], tuned to this 
application, could include an "add zero" constructor.