lambda calculus. The reason is that each different numberal has a
different type! For instance, if zero has type σ, then `false`
has type τ --> τ --> &tau, for some τ. Since one is
-represented by the function `\x.x false 0`, one must have type `(τ
---> τ --> &tau) --> &sigma --> σ`. But this is a different
+represented by the function `\x.x false 0`, one must have type (τ
+--> τ --> τ) --> σ --> σ. But this is a different
type than zero! Because each number has a different type, it becomes
impossible to write arithmetic operations that can combine zero with
one. We would need as many different addition operations as we had