coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ordinal induction

From: Danko Ilik <dankoilik AT gmail.com>
To: Edsko de Vries <Edsko.de.Vries AT cs.tcd.ie>
Cc: coq-club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Ordinal induction
Date: Thu, 22 Oct 2009 07:56:22 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to:x-mailer; b=nzxh44ro4p8Kt6gz2SKxMR3npX6FXewCCoE1f7w4m9TgwmaswGFEHI6Mp+u1YbTFhr Ff9Pg2GJLMrpyl8f3XHGlYQb6AKg3OYPKFQFCuroClA3m1bu8vuo6woOEVItBFrOk7/W 01Omt994Y3PBqbOvxVWmtzLywrZRq43Hp2KOs=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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?)

Maybe this coq contrib is relevant:
http://coq.inria.fr/distrib/current/contribs/Cantor.html

--
Danko Iliḱ

[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