coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT cs.berkeley.edu>
- To: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club]Set comprehensions in Coq?
- Date: Sat, 03 Mar 2007 18:22:56 -0800
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Peter Hawkins wrote:
No, I don't think that's what I want. If I understand things
correctly, that's a dependent type that lets me describe the type of
elements satisfying a predicate. I want _all_ elements satisfying a
predicate (as a concrete set), so I can, for example, write theorems
about properties of the set. Normally I'd want a value in Set, but I
don't think that's possible here.
'sig' does build Sets, and the resulting types have sets of values that are isomorphic to any other implementations of this idea that I can think of. Maybe if you give a concrete example of something that is too much of a pain to do using 'sig', I could suggest something else; or maybe some other reader of this list understands your purpose better.
- [Coq-Club]Set comprehensions in Coq?, Peter Hawkins
- Re: [Coq-Club]Set comprehensions in Coq?,
Adam Chlipala
- Re: [Coq-Club]Set comprehensions in Coq?,
Peter Hawkins
- Re: [Coq-Club]Set comprehensions in Coq?, Adam Chlipala
- Re: [Coq-Club]Set comprehensions in Coq?,
Peter Hawkins
- Re: [Coq-Club]Set comprehensions in Coq?, Adam Chlipala
- Re: [Coq-Club]Set comprehensions in Coq?, Benjamin Werner
- Re: [Coq-Club]Set comprehensions in Coq?,
Peter Hawkins
- Re: [Coq-Club]Set comprehensions in Coq?, Adam Chlipala
- Re: [Coq-Club]Set comprehensions in Coq?,
Peter Hawkins
- Re: [Coq-Club]Set comprehensions in Coq?,
Adam Chlipala
Archive powered by MhonArc 2.6.16.