diff options
| author | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-11 22:13:33 -0300 |
|---|---|---|
| committer | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-11 22:13:33 -0300 |
| commit | 5d967951eb0b08c36ee59f70d7f4cca37b0ca72b (patch) | |
| tree | f9265c6774f893f10cabc898f2838d40156b3c29 /lib/builtin.ml | |
| parent | 0886f3c71cf8551e4f8b3726654003a4f29645f0 (diff) | |
| download | SOL-5d967951eb0b08c36ee59f70d7f4cca37b0ca72b.tar.gz SOL-5d967951eb0b08c36ee59f70d7f4cca37b0ca72b.zip | |
world relation as the universe for scoped negation
Diffstat (limited to '')
| -rw-r--r-- | lib/builtin.ml | 4 |
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 |