The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

Hello, 

Thank you for the explanations. 

> My suggestion would be as follows :
> 
> - Streams (and generally coinductive types) should be defined something
> along the lines of :
> CoInductive Stream (A:Type) := { hd : A ; tl : Stream A }

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) }
 
> - 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?

Kind regards,
Keiko