Definition 1.3.3 (Full STlambdaC). The types of the full simply typed $\lambda$-calculus are generated by the following grammar:

$$\mathrm{\Pi }:=U|\mathrm{\Pi }\to \mathrm{\Pi }|\mathrm{\Pi }\times \mathrm{\Pi }|\mathrm{\Pi }+\mathrm{\Pi }|0|1,$$

where $U$ is a set of type variables (usually countable).

Its terms are given by ${\mathrm{\Lambda }}_{\mathrm{\Pi }}$ given by:

$${\mathrm{\Lambda }}_{\mathrm{\Pi }}:=V|\lambda V:\mathrm{\Pi }.{\mathrm{\Lambda }}_{\mathrm{\Pi }}|{\mathrm{\Lambda }}_{\mathrm{\Pi }}{\mathrm{\Lambda }}_{\mathrm{\Pi }}|{\mathrm{\Pi }}_1({\mathrm{\Lambda }}_{\mathrm{\Pi }})|{\mathrm{\Pi }}_2({\mathrm{\Lambda }}_{\mathrm{\Pi }})|{\iota }_1({\mathrm{\Lambda }}_{\mathrm{\Pi }})|{\iota }_2({\mathrm{\Lambda }}_{\mathrm{\Pi }})|\mathrm{case}({\mathrm{\Lambda }}_{\mathrm{\Pi }};V.{\mathrm{\Lambda }}_{\mathrm{\Pi }};V.{\mathrm{\Lambda }}_{\mathrm{\Pi }})|\ast |{!}_{\mathrm{\Pi }}{\mathrm{\Lambda }}_{\mathrm{\Pi }},$$

where $V$ is an infinite set of variables, and $\ast$ is a constant.