### Type Checking

<!--- data values--->
$\Huge
\frac{}{G\ \vdash\ \text{true}\ :\ bool}
\quad
\frac{}{G\ \vdash\ \text{false}\ :\ bool}
\quad
\frac{}{G\ \vdash\ n\ :\ int}$

<!--- plus --->
$\Huge \frac{G\ \vdash\ e_1\ :\ int\ \quad G\ \vdash\ e_2\ :\ int}{G\ \vdash\ e_1\ +\ e_2\ :\ int\ }$

<!--- and --->
$\Huge \frac{G\ \vdash\ e_1\ :\ bool\ \quad G\ \vdash\ e_2\ :\ bool\ }{G\ \vdash\ e_1\ \&\& \ e_2\ :\ bool\ }$

<!-- if -->
$\Huge \frac{G\ \vdash\ e_1\ :\ bool\ \quad G\ \vdash\ e_2\ :\ t\ \quad G\ \vdash\ e_3\ :\ t\ }{G\ \vdash\ \text{if}\ e_1\ \text{then}\ e_2\ \text{else}\ e_3\ :\ t\ }$

<!-- fun -->
$\huge \frac{G,x:t_1\ \vdash\ e\ :\ t_2 }{G\ \vdash\ \text{fun}\ (x\ :\ t_1)\ \rightarrow\ e\ :\ t_1\ \rightarrow t_2\ }$

<!-- lookup -->
$\huge \frac{}{G\ \vdash\ x\ :\ G(x)\ }$

<!-- let -->
$\huge \frac{G\ \vdash\ e_1\ : t_1\
\quad
G,x:t_1\ \vdash\ e_2\ : t_2\ }
{G\ \vdash\ \text{let}\ x\ =\ e_1\ \text{in}\ e_2\ :\ t_2\ }$

Example 1a: Use type checking to prove that this is well-typed:

`let a = true in a && false`
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
Example 1b: Use type checking to prove that this is well-typed:

`fun (z:int) -> z + 1`
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\

### Type Inference

<!--- data values--->
$\Huge
\frac{}{G\ \vdash\ \text{true}\ :\ bool\ \dashv\ \{\}}
\quad
\frac{}{G\ \vdash\ \text{false}\ :\ bool\ \dashv\ \{\}}
\quad
\frac{}{G\ \vdash\ n\ :\ int\ \dashv\ \{\}}$

<!--- plus --->
$\Huge \frac{G\ \vdash\ e_1\ :\ t_1\ \dashv\ C_1\quad G\ \vdash\ e_2\ :\ t_2\ \dashv\ C_2}{G\ \vdash e_1\ +\ e_2\ :\ int\ \dashv\ \{t_1:t_2,\ t_1: int\}\ \cup\ C_1\ \cup\ C_2}$

<!--- and --->
$\Huge \frac{G\ \vdash\ e_1\ :\ t_1\ \dashv\ C_1\quad G\ \vdash\ e_2\ :\ t_2\ \dashv\ C_2}{G\ \vdash e_1\ \&\& \ e_2\ :\ bool\ \dashv\ \{t_1:t_2,\ t_1: bool\}\ \cup\ C_1\ \cup\ C_2}$

<!-- if -->
$\Huge \frac{G\ \vdash\ e_1\ :\ t_1\ \dashv\ C_1 \quad G\ \vdash\ e_2\ :\ t_2\ \dashv\ C_2 \quad G\ \vdash\ e_3\ :\ t_3\ \dashv\ C_3}{G\ \vdash\ \text{if}\ e_1\ \text{then}\ e_2\ \text{else}\ e_3\ :\ t_2\ \dashv\ \{t_1:bool,\ t_2:t_3\}\ \cup\ C1\ \cup\ C_2\ \cup\ C_3}$

<!-- fun -->
$\huge \frac{\text{make}(t_x) \quad G,x:t_x\ \vdash\ e\ :\ t\ \dashv\ C_1}{G\ \vdash\ \text{fun}\ x\ \rightarrow\ e\ :\ t_x\ \rightarrow t\ \dashv\ C_1}$
(make creates some new, not yet used 'a/'b/'c-style type)

<!-- lookup -->
$\huge \frac{}{G\ \vdash\ x\ :\ G(x)\ \dashv\ \{\}}$

<!-- let -->
$\huge \frac{G\ \vdash\ e_1\ : t_1\ \dashv\ C_1
\quad
G,x:t_1\ \vdash\ e_2\ : t_2\ \dashv\ C_2}
{G\ \vdash\ \text{let}\ x\ =\ e_1\ \text{in}\ e_2\ :\ t_2\ \dashv\ C_1\ \cup\ C_2}$

Example 2a: Use type inference to prove that this is well-typed:

`let a = true in a && false`
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
Example 2b: Use type inference to prove that this is well-typed:

`fun z -> z + 1`
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
___________

Example(s) with just let bindings and &&:


Example(s) with functions and +: