[Agda] A plea for Set:Set

[Ulf Norell]

On Fri, May 16, 2008 at 11:37 PM, Remi Turk <rturk at science.uva.nl> wrote:

> On Tue, May 13, 2008 at 09:42:50PM +0000, Thorsten Altenkirch wrote:
> >
> > On 13 May 2008, at 22:37, Samuel Bronson wrote:
> >
> > > On Tue, May 13, 2008 at 3:43 PM, Nils Anders Danielsson
> > > <nils.anders.danielsson at gmail.com> wrote:
> > >> The flag turns off the universe check when you define data types and
> > >> record types. However, Set1 still does not match Set.
> > >
> > > What is the price for this?
> >
> > You have to pay the equivalent of EUR 1.50 into the Russell Memorial
> > Fund, each time you use it. For details see
> > http://en.wikipedia.org/wiki/Russell%27s_paradox
>
> Don't we already have to pay this in current Agda on
> architectures with a finite word size?
>
> Main> :typeOf Set2147483647
> Set-2147483648
>
> Main> :typeOf Set-2147483648
> 1,1-15
> Not in scope:
>  Set-2147483648 at 1,1-15
> when scope checking Set-2147483648
>
> Main> :typeOf Set2147483648
> Set-2147483647
>
> Main> :typeOf Set4294967294
> Set-1
>
> Main> :typeOf Set4294967295
> Set
>
> In other words:
>
> Set : Set1 : ... : SetMAXINT : SetMININT : ... Set-1 : Set


Oops... :-)

I'll change that Int to Integer.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080517/04de0544/attachment-0001.html