--- a/doc/source/logic_tricks.txt +++ b/doc/source/logic_tricks.txt @@ -126,32 +126,14 @@ For example: for all $x from generate_x($x), test_y($x) is true -Rethink this as a combination of two negatives on ``exists``, above: there -does *not* ``exist`` an ``$x`` from ``generate_x($x)`` where ``test_y($x)`` is -*not* true. Then combine the ``not`` trick with the ``exists`` trick. -This needs a new subgoal, we'll call it ``for_all_x``:: +Use the forall clause:: - for_all_x_failure: - use for_all_x() - when - generate_x($x) # these two lines are the exists trick - not_test_y($x) - special.claim_goal() # don't use any other rules for for_all_x - check False # and cause this rule to fail, which causes the for_all_x goal to fail + forall + generate_x($x) + require + test_y($x) - for_all_x_success: - use for_all_x() # we only make it here if all generated $x values have test_y($x) true +Note that all pattern variable bindings done in the forall clause are undone +before the next clause is run. -Then you also need to create rules for the ``not_test_y`` goal using the -``not`` trick, above:: - - not_test_y_fail: - use not_test_y($x) - when - test_y($x) # if there is any way for test_y($x) to be true - special.claim_goal() # don't use any other rules for not_test_y - check False # and cause this rule to fail, which causes the not_test_y goal to fail - - not_test_y_success: - use not_test_y($_) # this rule only runs if test_y($x) fails, above - +This always fails on backtracking.