[Agda] A plea for Set:Set

[Remi Turk]

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

Groeten, Remi