evaluates to? Well, consider the right-hand side of the second binding:
- let
- x match x + 1
- in (x, 2*x)
+ let
+ x match x + 1
+ in (x, 2*x)
This expression evaluates to `(1, 2)`, because it uses the outer binding of `x` to `0` for the right-hand side of its own binding `x match x + 1`. That gives us a new binding of `x` to `1`, which is in place when we evaluate `(x, 2*x)`. That's why the whole thing evaluates to `(1, 2)`. So now returning to the outer expression, `y` gets bound to `1` and `z` to `2`. But now what is `x` bound to in the final line,`([y, z], x)`? The binding of `x` to `1` was in place only until we got to `(x, 2*x)`. After that its scope expired, and the original binding of `x` to `0` reappears. So the final line evaluates to `([1, 2], 0)`.
-This is very like what happens in ordinary predicate logic if you say: ∃ `x. F x and (` ∀ `x. G x ) and H x`. The `x` in `F x` and in `H x` are governed by the outermost quantifier, and only the `x` in `G x` is governed by the inner quantifier.
+This is very like what happens in ordinary predicate logic if you say:
+
+∃ `x. F x and (` ∀ `x. G x ) and H x`
+
+The `x` in `F x` and in `H x` are governed by the outermost quantifier, and only the `x` in `G x` is governed by the inner quantifier.
### That's enough ###