# Monotype Proof Tree Editor

# Monotype Derivation

Write a proof tree for the following judgement:

$\Gamma \vdash \mathtt{if}\ f\ 0 \ge 0 \ \mathtt{then}\ f\ \mathtt{else}\ (\lambda x.\ x) : Int \to Int$

Let $f : Int \rightarrow Int$ in $\Gamma$.

Each line of your tree should have the following components:

- a number followed by a period to indicate its depth in the tree. 0 is the root.
- a Gamma, in the form
`G`,`G$n$`(where $n$ is an integer) or as a set of variable type assignments. - The
`|-`

operator. - An expression.
- The
`:`

operator. - A type name. Type names are capitalized.
- A rule name in parenthesis.

If you use `G` or `G1`, etc. in your proof tree, you must
follow the tree with their expanded out definitions.

The starter code shows a valid tree for a proof of $\Gamma \vdash x + y : Int$.

Here are the monotype rules.

# Proof Tree Editor

Score: 17.61%

$\frac{\frac{}{\displaystyle \Gamma\vdash x : Int} \textstyle \mathrm{V\small{AR}} \quad \frac{}{\displaystyle \Gamma\vdash y : Int} \textstyle \mathrm{V\small{AR}}}{\displaystyle \Gamma\vdash x + y : Int}\textstyle \mathrm{B\small{INOP}}$