The Coq mailing list

[Benjamin Werner <werner AT lix.polytechnique.fr>]

  Hello,

Again, sorry for the late reply.

> > Inductive Ord : Type :=
> >  Ord_cons : (I:Type) (I -> Ord) -> Ord.
>
> I realised that this is exactly the "Ens" type of sets in Benjamin
> Werner's encoding of ZF set theory in Coq (contrib Rocq/ZF). I created
> my Conway Games type by taking inspiration from Ens, so "la boucle est
> bouclée".

In general it depends of what ordinals you want to deal with. You can get 
a subset of the set-theoretical ordinals with the well-known example (but 
Pierre is certainly aware of that) :

Inductive Ord : Type :=
   O_Ord : Ord
 | S_ord : Ord -> Ord
 | lim_Ord : (nat->Ord) -> Ord.

Which is a form of ordinal notation.

When considering ordinals like in set-theory, the problem is that the 
usual definition is fundamentally classical (ordinals are sets which, 
among other things, have the property that their elements are totaly 
ordered wrt. membership).

Paul Taylor has a big paper where he develops ordinals constructively. On 
the other hand, he heavily relies on impredicativity. A few years back, I 
adapted his developement into Coq (on top of the Ens type) and it works 
quite well. I did not know what to do with this and have not advertized 
this work. If you think you have a use for it, I would be happy to talk 
about it.


Amities,


Benjamin