Type Rules for Block Statement

Note that variable declarations are allowed in blocks

we type statements one by one
declarations introduce new bindings into the environment

We apply these rules (with those listed first having higher priority):

$\begin{equation*} \Gamma \vdash \{\} : void \end{equation*}$

$\begin{equation*} \frac{\Gamma \vdash e : T} {\Gamma \vdash \{\textbf{return}\ e\} : T} \end{equation*}$

$\begin{equation*} \frac{\Gamma \oplus \{x \mapsto T_1\} \vdash \{ s_2 \ldots\ s_n\} : T} {\Gamma \vdash \{ T_1\, x; s_2\ \ldots\ s_n \} : T} \end{equation*}$

$\begin{equation*} \frac{\Gamma \vdash s_1 : void,\ \Gamma \vdash \{ s_2 \ldots\ s_n\} : T} {\Gamma \vdash \{ s_1\ s_2\ \ldots\ s_n \} : T} \end{equation*}$