[Agda] Universe polymorphism

[Ulf Norell]

On Fri, Sep 25, 2009 at 7:33 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk>wrote:

> On 2009-09-25 17:17, Ulf Norell wrote:
>
>>  or set it in the emacs mode options.
>>
>
> How?


Hm, I thought there was some way to give command line arguments in the emacs
options, I guess I was wrong.


>  The type Level is isomorphic to the unary natural numbers and should be
>>  specified using the BUILTINs LEVEL, LEVELZERO, and LEVELSUC:
>>
>
> Is there any reason not to bind LEVEL to ℕ?


There are some special rules for checking equality between levels (for
instance max i i = i) and I didn't want those interfering with normal
programs with natural numbers. Also, keeping levels as a separate type will
make it easier to change it if we wanted to. For instance, non-uniformity
might be more trouble than it's worth.

Binding LEVEL to the same type as NATURAL will make things break
spectacularly (I believe). There should be a check that you don't do that,
but it's not implemented yet.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20090925/dd5403c9/attachment.html