Start working on case expression rule

content/blog/03_compiler_trees.md

@@ -243,3 +243,49 @@ types that satisfy the rules.
 #### Checking More Expressions
 So far, we've only checked types of numbers, applications, and variables.
 Our language has more than that, though!
+
+Binary operators are by far the simplest to extend our language with;
+We can simply say that `(+)` is a function, `Int -> Int -> Int`, and
+`x+y` is the same as `(+) x y`. This way, we simply translate
+operators into function application, and the same typing rules apply.
+
+Next up, we have case expressions. This is one of the two places
+where we will introduce new variables into the context, and
+also a place where we will need several rules.
+
+Let's first take a look at the whole case expression rule:
+{{< todo >}} Double check squiggly notation. {{< /todo >}}
+$$
+\\frac
+{\\Gamma \\vdash e : \\tau \\quad \\tau | p\_i \\leadsto b\_i \\quad \\Gamma,b\_i \\vdash e\_i : \\tau\_c}
+{\\Gamma \\vdash \\text{case} \\; e \\; \\text{of} \; \\\{ (p\_1,e\_1) \\ldots (p\_n, e\_n) \\\} : \\tau\_c }
+$$
+This is a lot more complicated than the other rules we've seen, and we've used some notation
+that we haven't seen before. Let's take this step by step:
+
+1. \\(e : \\tau\\), in this case, means that the expression between `case` and `of`, is of type \\(\\tau\\).
+2. \\(\\tau | p\_i \\leadsto b\_i\\) means that the pattern \\(p\_i\\) can match a value of type
+\\(\\tau\\), producing additional type pairs \\(b\_i\\). We need \\(b\_i\\) because a pattern
+such as `Cons x xs` will introduce new type information, namely \\(\text{x} : \text{Int}\\) and \\(\text{xs} : \text{List}\\).
+3. \\(\\Gamma,b\_i \\vdash e\_i : \\tau\_c\\) means that each individual branch can be deduced to have the type
+\\(\\tau\_c\\), using the previously existing context \\(\\Gamma\\), with the addition of \\(b\_i\\), the new type information.
+4. Finally, the conclusion is that the case expression, if all the premises are met, is of type \\(\\tau\_c\\).
+
+For completeness, let's add rules for \\(\\tau | p\_i \\leadsto b\_i\\). We'll need two: one for
+the "basic" pattern, which always matches the value and binds it to the variable, and one
+for a constructor pattern, that matches a constructor and its parameters.
+
+Let's define \\(v\\) to be a variable name in the context of a pattern. For the basic pattern:
+$$
+\\frac
+{}
+{\\tau | v \\leadsto \\\{v : \\tau \\\}}
+$$
+
+{{< todo >}} consult pierce. {{< /todo >}}
+The rule for the constructor pattern, then, is:
+$$
+\\frac
+{}
+{}
+$$