The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Thu, Sep 09, 2004 at 03:47:45PM +0200, Lionel Elie Mamane wrote:
> On Tue, Sep 07, 2004 at 10:36:43AM +0200, 
>Â casteran AT labri.fr
>  wrote:

>>   I am looking for any development in Coq allowing to work with
>> ordinal numbers.

> Depending on how concrete you want to really get, it might pay off to
> "slaughter down" my Conway Games type down to something that would
> make acceptable ordinals. I'm thinking of something along the lines
> of:

> 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".

-- 
Lionel