X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;f=hints%2Fassignment_7_hint_3.mdwn;h=59682986299494ce90eb386c7be21780d76301df;hb=d6ac33904ee6021cad8e517d4f5104c3b82f1570;hp=4a159e9e487dce7aebbf4a7cf758df814f3bbfe4;hpb=157b0b898f07c15b13e42718fab380c4ee69d7ea;p=lambda.git

diff --git a/hints/assignment_7_hint_3.mdwn b/hints/assignment_7_hint_3.mdwn
index 4a159e9e..59682986 100644
--- a/hints/assignment_7_hint_3.mdwn
+++ b/hints/assignment_7_hint_3.mdwn
@@ -27,9 +27,9 @@ More specifically, \[[expression]] will be a set of `'a discourse_possibility` m
 				(* the reason for returning a triple with () in first position will emerge *)
 				in ((), r',g')
 
-*	At the top of p. 13 (this is in between defs 2.8 and 2.9), GS&V give two examples, one for \[[∃xPx]] and the other for \[[Qx]]. In fact it will be easiest for us to break \[[∃xPx]] into two pieces, \[[∃x]] and \[[Px]]. Let's consider expressions like \[[Px]] (or \[[Qx]]) first.
+*	At the top of p. 13 (this is in between defs 2.8 and 2.9), GS&V give two examples, one for \[[∃xPx]] and the other for \[[Qx]]. In fact it will be easiest for us to break \[[∃xPx]] into two pieces, \[[∃x]] and \[[Px]]. Let's consider expressions like \[[Px]]  first.
 
-	They say that the effect of updating an information state `s` with the formula `Qx` should be to eliminate possibilities in which the object associated with the peg associated with the variable `x` does not have the property Q. In other words, if we let `Q` be a function from objects to `bool`s, `s` updated with \[[Qx]] should be `s` filtered by the function `fun (r, g) -> let obj = List.nth g (r 'x') in Q obj`.
+	They say that the effect of updating an information state `s` with the meaning of "Qx" should be to eliminate possibilities in which the object associated with the peg associated with the variable `x` does not have the property Q. In other words, if we let `Q` be a function from objects to `bool`s, `s` updated with \[[Qx]] should be `s` filtered by the function `fun (r, g) -> let obj = List.nth g (r 'x') in Q obj`. When `...Q obj` evaluates to `true`, that `(r, g)` pair is retained, else it is discarded.
 
 	Recall that [we said before](/hints/assignment_7_hint_2) that `List.filter (test : 'a -> bool) (u : 'a set) : 'a set` is the same as:
 
@@ -41,15 +41,17 @@ More specifically, \[[expression]] will be a set of `'a discourse_possibility` m
 
 	We can call the `(fun (r, g) -> ...)` part \[[Qx]] and then updating `s` with \[[Qx]] will be:
 
-		bind_set s [[Qx]]
+		bind_set s \[[Qx]]
 
 	or as it's written using Haskell's infix notation for bind:
 
-		s >>= [[Qx]]
+		s >>= \[[Qx]]
 
 *	Now how shall we handle \[[∃x]]. As we said, GS&V really tell us how to interpret \[[∃xPx]], but what they say about this breaks naturally into two pieces, such that we can represent the update of `s` with \[[∃xPx]] as:
 
-		s >>= [[∃x]] >>= [[Px]]
+<pre><code>
+s >>= \[[&exist;x]] >>= \[[Px]]
+</code></pre>