The Coq mailing list

[roconnor AT theorem.ca]

On Sat, 7 Jun 2008, 
roconnor AT theorem.ca
 wrote:

> But I worry that there are (as you say) more snakes.  CoInductive types are 
> very strange.  They are the only objects where computation "simplfies" the 
> introduction rule (cofix) rather than simplifying the elimination rule.

I think I'm wrong about this point.  match is the eliminator and cofix is 
the introducution (with cons being a sort of degenerate cofix).  This 
makes match (cofix ...) ... a redex, which indeed seems to be what Coq 
does.

My reference on CoInductive types is just one section from "Type Theory 
and Functional Programming" (where his "computation rule" operated on 
the cofix).  What is the reference that details the rules for coinductive 
types in Coq?

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''