\frac{<b, σ> → true <c_1, σ> → σ'}{<\text{if } b \text{ then }c_1 \text{ else } c_2,σ> → σ'}
```
```math
\frac{<b, σ> → false <c_2, σ> → σ'}{<\text{if } b \text{ then }c_1 \text{ else } c_2,σ> → σ''}
\frac{<b, σ> → false <c_2, σ> → σ''}{<\text{if } b \text{ then }c_1 \text{ else } c_2,σ> → σ''}
```
``` rust
...
...
@@ -426,9 +426,77 @@ while a < 10 {
## Your type checker
> - Give a simplified set of Type Checking Rules for your language (those rules look very much like the SOS rules, but over types not values). Also here you don't need to detail rules that are similar (follow the same pattern).
> - Demonstrate each "type rule" by an example. You may use one or several "programs" to showcase where rules successfully apply.
> - For your implementation, give a set of programs demonstrating that ill-typed programs are rejected, connect back to the Type Checking Rules to argue why these are illegal and thus should be rejected.
> - Compare your solution to the requirements (as stated in the README.md). What are your contributions to the implementation.