[Agda] A plea for Set:Set

[Thorsten Altenkirch]

Thanks a lot, Ulf.

Also Hurkens.agda will be extremely useful to prove hard theorems,  
like P != NP, or P=NP, as you like.... :-)

Cheers,
Thorsten

On 14 May 2008, at 12:40, Ulf Norell wrote:

>
> On Wed, May 14, 2008 at 2:21 AM, Nils Anders Danielsson <nils.anders.danielsson at gmail.com 
> > wrote:
>
> If you really want to implement Hurkens' paradox...
>
> I changed --no-universe-check to --type-in-type and changed the  
> semantics to the real thing. Hurkens' paradox goes through straight  
> from the paper [1].
>
> I added the paradox to the test suite in test/succeed/Hurkens.agda.
>
> / Ulf
>
> [1] A. Hurkens, A simplification of Girard's paradox. In the  
> proceedings of TLCA '95. (c) Springer Verlag.
>
> <Hurkens.agda>_______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080516/a4ff6e81/attachment.html