The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

Hello there,

What is "sig", and how to construct values of "sig" seems clear.

I am trying to wrap my head around "sigT".
https://coq.inria.fr/library/Coq.Init.Specif.html#sigT

This seems to be simple enough example term:

        {n : nat & {m : nat | n < m}}

Coq says that it has type Set.

I am trying to figure out:

  1. what that set represents

  2. how can I construct elements of that Set.


I am sorry about asking trivialities here.

Thank you in advance for the help.