The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Robert Dockins wrote:

> That said, there are some of the more esoteric  areas that Coq'Art 
> doesn't cover.  For example, there is an important  restriction on 
> inductive definitions called some thing like the  "positivity 
> requirement" which I could not find in Coq'Art; I had to  dig around 
> in the documentation and finally read a journal paper  before I found 
> a satisfactory explanation of what this restriction is  and why it 
> exists.


Well, There is some stuff about that pp 389-390, and more examples in 
the Tutorial on [co-]inductive
types (reachable from Coq's documentation page : look at  "Additional 
Documentation").

Speaking about I/O, there is probably some interesting work [to be ?] 
done using co-inductive types for
representing I/O streams, but I don't have any precise links.

Pierre



> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club