The Coq mailing list

[Nils Anders Danielsson <nad AT Cs.Nott.AC.UK>]

On 2009-10-21 16:49, Edsko de Vries wrote:
> Also, if I can ask a potentially very stupid question: is there a 
> relation between ordinal induction and coinduction?

A function from the natural numbers can be seen as a coinductively
defined structure. Peter Hancock recently mentioned the following
definition of the Brouwer ordinals:

 mu X. nu Y. 1 + X * Y

 (http://article.gmane.org/gmane.comp.lang.agda/953)

--
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.