coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Ordinal induction, Edsko de Vries
- Re: [Coq-Club] Ordinal induction,
Dan Doel
- Re: [Coq-Club] Ordinal induction,
Edsko de Vries
- Re: [Coq-Club] Ordinal induction,
Dan Doel
- Re: [Coq-Club] Ordinal induction, Edsko de Vries
- Re: [Coq-Club] Ordinal induction,
Dan Doel
- Re: [Coq-Club] Ordinal induction,
Edsko de Vries
- Re: [Coq-Club] Ordinal induction, Danko Ilik
- Re: [Coq-Club] Ordinal induction, Nils Anders Danielsson
- Re: [Coq-Club] Ordinal induction,
Dan Doel
Archive powered by MhonArc 2.6.16.