world relation as the universe for scoped negation

1 files changed, 8 insertions, 0 deletions

diff --git a/test/test_vm.ml b/test/test_vm.ml
index 83532d6..0ae62e1 100644
--- a/test/test_vm.ml
+++ b/test/test_vm.ml
@@ -203,6 +203,12 @@ let test_negation_defers_until_ground () =
    ^ {| Query expression: ([Adult name: N] :not [Equal left: N right: "Rui"]) :and [Person name: N age: A] |})
     {|N="Marcos",A=30|}
 
+let test_world_scoped_negation () =
+  (* The specification's own negation form. *)
+  check_answers "no adult named Ana"
+    (people ^ {| Query expression: [World] :not [Adult name: "Ana"] |})
+    ""
+
 (* Quantifiers. *)
 
 let test_forall_holds () =
@@ -359,6 +365,8 @@ let () =
           Alcotest.test_case "not adults" `Quick test_negation;
           Alcotest.test_case "denial defers until ground" `Quick
             test_negation_defers_until_ground;
+          Alcotest.test_case "world-scoped negation" `Quick
+            test_world_scoped_negation;
         ] );
       ( "quantifiers",
         [