aboutsummaryrefslogtreecommitdiffstats
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/builtin.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/builtin.ml b/lib/builtin.ml
index 694b688..082471b 100644
--- a/lib/builtin.ml
+++ b/lib/builtin.ml
@@ -13,6 +13,7 @@ let upper_l = forced_label "upper"
let names =
[
"True";
+ "World";
"Integer";
"Natural";
"Rational";
@@ -143,6 +144,9 @@ let between subst bindings =
let run subst name bindings =
match name with
| "True" -> Some (yes subst)
+ (* The universe: true of every tuple, per the specification. Its
+ role is to scope denial, as in [World] :not [Adult person: P]. *)
+ | "World" -> Some (yes subst)
| "Integer" ->
Some
(domain_check subst bindings (function