X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week1.mdwn;h=24d606b2a4ced242f0a37f96e904c339e8bb19e0;hp=b724a1ba944b2ca0d7792469d8d2428710aec5c1;hb=b6ecb9372e9895e6b8d49e054ed90ff69a87c247;hpb=edccef45f1546218646487c5f1c779a8f7c380fe

diff --git a/week1.mdwn b/week1.mdwn
index b724a1ba..24d606b2 100644
--- a/week1.mdwn
+++ b/week1.mdwn
@@ -594,13 +594,17 @@ the variable `x` has not been *overwritten* (mutated). Rather, we have *two* var
 
 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 ###