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 |