The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

On Feb 20, 2006, at 1:37 AM, Pierre Casteran wrote:

> 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").

Perhaps you have a different edition than me.  Pages 389-390 in my  
edition are in section 14.1.4, a subsection titled "Dependently Typed  
Recursors".  However, a little page flipping brings me to section  
14.1.2.2, which is see does discuss positivity, albeit fairly  
briefly.  So, I retract that particular critique.


On a side note, is there any good tutorial/didactic material dealing  
with Coq's implicit coercion system?  I find the documentation very  
difficult to read and Coq'Art doesn't cover it.


Rob Dockins

Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
          -- TMBG