week1 refinements

diff --git a/topics/week1.mdwn b/topics/week1.mdwn
index 24d606b..0bbea4e 100644 (file)
--- a/topics/week1.mdwn
+++ b/topics/week1.mdwn
@@ -134,7 +134,7 @@ It's okay to also write it all inline, like so: `let x be 5; y be x + 1 in 2 * y
 
 The `x + 1` that is evaluated to give the value that `y` gets bound to uses the (more local) binding of `x` to `5`, not the (previous, less local) binding of `x` to `0`. By the way, the parentheses in that displayed expression were just to focus your attention. It would have parsed and meant the same without them.
 
 
 The `x + 1` that is evaluated to give the value that `y` gets bound to uses the (more local) binding of `x` to `5`, not the (previous, less local) binding of `x` to `0`. By the way, the parentheses in that displayed expression were just to focus your attention. It would have parsed and meant the same without them.
 

-Now we can allow ourselves to introduce λ-expressions in the following way. If a λ-expression is applied to an argument, as in: `(`λ `x.` φ`) M`, for any (simple or complex) expressions φ and `M`, this means the same as: `let x be M in` φ. That is, the argument to the λ-expression provides (when evaluated) a value for the variable `x` to be bound to, and then the result of the whole thing is whatever φ evaluates to, under that binding to `x`.
+Now we can allow ourselves to introduce λ-expressions in the following way. If a λ-expression is applied to an argument, as in: `(`λ `x.` φ`) M`, for any (simple or complex) expressions φ and `M`, this means the same as: `let x be M in` φ. That is, the argument `M` to the λ-expression provides (when evaluated) a value for the variable `x` to be bound to, and then the result of the whole thing is whatever φ evaluates to, under that binding to `x`.

 
 If we restricted ourselves to only that usage of λ-expressions, that is when they were applied to all the arguments they're expecting, then we wouldn't have moved very far from the decidable fragment of arithmetic we began with.
 
 
 If we restricted ourselves to only that usage of λ-expressions, that is when they were applied to all the arguments they're expecting, then we wouldn't have moved very far from the decidable fragment of arithmetic we began with.
 


@@ -383,7 +383,7 @@ is a pattern, meaning the same as `x1 & x2 & []`. Note that while `x & xs` match
 For the time being, these are the only patterns we'll allow. But since the definition of patterns is recursive, this permits very complex patterns. What would this evaluate to:
 
     let
 For the time being, these are the only patterns we'll allow. But since the definition of patterns is recursive, this permits very complex patterns. What would this evaluate to:
 
     let

-      ([x, y], [z:zs, w]) match ([[], 'true], [[10, 20, 30], 'false])
+      ([x, y], [z:zs, w]) match ([[], [1]], [[10, 20, 30], [0]])

     in (z, y)
 
 Also, we will permit complex patterns in λ-expressions, too. So you can write:
     in (z, y)
 
 Also, we will permit complex patterns in λ-expressions, too. So you can write: