[Agda] A plea for Set:Set

[Samuel Bronson]

On Tue, May 13, 2008 at 6:10 PM, Wouter Swierstra <wss at cs.nott.ac.uk> wrote:

>  A variation of it has been written out in Coq:

It doesn't seem to work:

/home/naesten/hacking/haskell/Agda2/examples/Rustle.agda:29,30-31
Set2 != Set1
when checking that the expression U has type Set
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Rustle.agda
Type: application/octet-stream
Size: 823 bytes
Desc: not available
Url : https://lists.chalmers.se/mailman/private/agda/attachments/20080513/528a3022/Rustle.obj