Sum and product types in Coq

Sun, 28 Feb 2016 15:49:36 GMT

External Content not shown. Further Information.

As I always forget them, here a short list of functions regarding several sum- and product types in Coq. If I missed something, feel free to send me a comment.

Product types:

notation    | name     | left proj. | right proj. |
------------+----------+------------+-------------+
A /\ B      | and      | proj1      | proj2       |
A * B       | pair     | fst        | snd         |
{x | A}     | exist    | proj1_sig  | proj2_sig   |
{x : B & A} | existT   | projT1     | projT2      |

Sum Types:

notation    | name     | intro left | intro right |
------------+----------+------------+-------------+
A \/ B      | or       | or_introl  | or_intror   |
A + B       | sum      | inl        | inr         |
{A} + {B}   | sumbool  | left       | right       |