manip trees: more explanation
[lambda.git] / hints / assignment_7_hint_6.mdwn
index 77b4792..e513284 100644 (file)
                                        (* 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;;
 
 
+       **Thanks to Simon Charlow** for catching a subtle error in previous versions of this function. Fixed 1 Dec.
+
 *      Representing \[[and φ ψ]] is simple:
 
                let and_op (phi : clause) (psi : clause) : clause =
@@ -36,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) ->