[Agda] heterogeneous lists with universes

[J.Burton at brighton.ac.uk]

Hi Andres, thanks very much. As to what I'm trying to accomplish, I want to use these TSets (after making them behave like sets) in data structures holding terms in a formal language for reasoning with diagrams. So this way I can do some reasoning with the types as well as the terms. A simple example is adding a contour to a diagram -- you can add any contour that isn't already in the diagram, and the resulting diagram includes the new contour. I'll put this specification in the type.

Jim 


-----Original Message-----
From: Andres Loeh [mailto:andres at cs.uu.nl]
Sent: Wed 11/5/2008 5:31 PM
To: Burton James
Subject: Re: [Agda] heterogeneous lists with universes
 
Hi Jim.

I'm not quite sure what you really want to accomplish.
I've attached three versions of your code that typecheck.
The first is the simplest and doesn't need universes at
all. The second is probably closest to your code, and the
third is the one which I think is closest to being useful.

HTH,
  Andres

-- 

Andres Loeh, Universiteit Utrecht

mailto:andres at cs.uu.nl     mailto:mail at andres-loeh.de
http://www.andres-loeh.de

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