coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: Bas Spitters <spitters AT cs.ru.nl>
- Cc: Coq Club <coq-club AT inria.fr>, Venanzio Capretta <vxc AT cs.nott.ac.uk>
- Subject: Re: [Coq-Club] Tarski style universes in Coq
- Date: Wed, 29 Aug 2012 16:14:02 -0400
On 08/29/2012 04:05 PM, Bas Spitters wrote:
Is there any work trying to mimick Tarski style universes in Coq?
I.e. defining universes using explicit codes.
Do you just mean defining a type of syntax for types, or do you have a particular class of supported types in mind?
- [Coq-Club] Tarski style universes in Coq, Bas Spitters, 08/29/2012
- Re: [Coq-Club] Tarski style universes in Coq, Adam Chlipala, 08/29/2012
- Re: [Coq-Club] Tarski style universes in Coq, Bas Spitters, 08/30/2012
- Re: [Coq-Club] Tarski style universes in Coq, Adam Chlipala, 08/29/2012
Archive powered by MHonArc 2.6.18.