The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

Hi, I'm tring to understand sig, sigT, their differences and how to use they.

For example, i tried to define elements

Definition ex1:= (( [ ], (NoDup_nil nat)) :{x:list nat | NoDup x}).
Definition ex2:= (( [ ], (NoDup_nil nat)) :{x:list nat & NoDup x}).

but with no success.
How to define elements of type {x:list nat | NoDup x} or {x:list nat &
NoDup x} ? and what is the difference between this two types?

I have used up to now records wit a "proof" field for the same purpose
it this sig and sigT looks made for...

Thanks.
Marco.