[Agda] A plea for Set:Set

[Nils Anders Danielsson]

On Tue, May 13, 2008 at 8:34 PM, Thorsten Altenkirch <txa at cs.nott.ac.uk> wrote:
>
>  Sounds good. How to I use it via the emacs interface?

{-# OPTIONS --no-universe-check #-}

>  Why "almost"?

The flag turns off the universe check when you define data types and
record types. However, Set1 still does not match Set.

-- 
/NAD