manip trees: more explanation

[lambda.git] / hints / assignment_7_hint_6.mdwn

diff --git a/hints/assignment_7_hint_6.mdwn b/hints/assignment_7_hint_6.mdwn
index 38f6c2e..e513284 100644 (file)
--- a/hints/assignment_7_hint_6.mdwn
+++ b/hints/assignment_7_hint_6.mdwn
@@ -20,14 +20,14 @@
                                        (* if one_dpm isn't already false at (r, h),
                                           we want to check its behavior when updated with phi
                                           bind_set (unit_set one_dpm) phi === phi one_dpm; do you remember why? *)
-                                   let (truth_value, _, _) = one_dpm (r, h)
+                                   let (truth_value, r', h') = one_dpm (r, h)
                                        in let truth_value' = truth_value && (truths (phi one_dpm) (r, h) = [])
                                        (* new_dpm must return a (bool, r, h) *)
-                    in (truth_value', r, h)
+                    in (truth_value', r', h')
                                in unit_set new_dpm;;
 
 
-       **Note: Simon pointed out a subtle error in this code, which we will look into fixing. At the moment, the subtle error is still there.**
+       **Thanks to Simon Charlow** for catching a subtle error in previous versions of this function. Fixed 1 Dec.
 
 *      Representing \[[and φ ψ]] is simple:
 
@@ -38,6 +38,8 @@
 
 *      Here are `or` and `if`:
 
+       (These probably still manifest the bug Simon spotted.)
+
                let or_op (phi : clause) (psi : clause) =
             fun one_dpm -> unit_set (
                 fun (r, h) ->