Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Ordinal induction

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Ordinal induction


chronological Thread 
  • From: Edsko de Vries <Edsko.de.Vries AT cs.tcd.ie>
  • To: coq-club <coq-club AT pauillac.inria.fr>
  • Subject: [Coq-Club] Ordinal induction
  • Date: Wed, 21 Oct 2009 16:49:18 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

Is there an accessible reference to the use of ordinal induction in type theory? For example, an introduction to Brouwer ordinals and induction on them? (This would be ordinal induction, right?)

Also, if I can ask a potentially very stupid question: is there a relation between ordinal induction and coinduction?

Thanks,

Edsko





Archive powered by MhonArc 2.6.16.

Top of Page