The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

I am specifically interested in colists, i.e., potentially infinite lists
with Nil and Cons constructors; records seem to me a less natural
representation for colists. What I imagine is something like:

CoInductive Colists (A:Type) := { hd : A ; tl : Option (Colists A) }

This should work perfectly.
 

> - Do not use destruct or case or intros [ ] or whatever similar on a string
> object

When I deduce a coinductive property by coinduction,
I case analyze a coinductive object to get a constructor,
therefore to get a guarded coinduction. If I cannot move to records,
the absence of case and the likes sounds restrictive. Am I correct?

 

It might be. CoInductive defined as sums are difficult (if possible) to manipulate without pattern matching, it is fairly unclear to me how one could manipulate a CoInductive with several constructors. It is usually possible to encode them into records like you did for CoLists, but it's not necessarily satisfactory.



Arnaud