The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Marco Servetto wrote:
> 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?
>    

You've already done the hard work of figuring out which type family is 
matched with each of the different notations.  If you need to do that in 
the future, you might like to use the [Locate] command, illustrated like:
    Locate "{ _ : _ | _ }".

This command finds [sig].  Then you can run:
    Print sig.
...which will show you the type definition, including the single 
constructor and its type.  As far as I know, the standard library 
contains no shorthand syntax for applying this constructor, so you just 
call it directly (or define your own notation, as I often do).

If this advice is insufficient, please feel free to write again!

(The same advice should also make it possible to see the difference 
between [sig] and [sigT].)