[Agda] Universe polymorphism

[Nils Anders Danielsson]

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

How?

>   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 ℕ?

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.