Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club]Set comprehensions in Coq?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Set comprehensions in Coq?


chronological Thread 
  • 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.





Archive powered by MhonArc 2.6.16.

Top of Page