- (* we want to check the behavior of one_dpm when updated with the operation phi *)
- (* bind_set (unit_set one_dpm) phi === phi one_dpm; do you remember why? *)
- let truth_value' = truths (phi one_dpm) (r, h) = []
- (* we return a (bool, r, h) so as to constitute a dpm *)
- in (truth_value', r, h)
- in unit_set new_dpm
+ (* if one_dpm isn't already false at (r, h),
+ we want to check its behavior when updated with phi
+ set_bind (set_unit one_dpm) phi === phi one_dpm; do you remember why? *)
+ 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 set_unit new_dpm;;