[Agda] A plea for Set:Set

Nils Anders Danielsson nils.anders.danielsson at gmail.com
Wed May 14 14:19:37 CEST 2008


2008/5/14 Ulf Norell <ulfn at cs.chalmers.se>:
>
> I changed --no-universe-check to --type-in-type and changed the semantics to
> the real thing.

Nice. Do you have any plans for an "Agda commentary", to make it
easier for the rest of us to implement features like this one?

-- 
/NAD


More information about the Agda mailing list