4.6 Coinductive types

The implementation contains also coinductive definitions, which are types inhabited by infinite objects.

Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.0.3.5.html at 8/10/98