The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

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.