1 files changed, 40 insertions, 0 deletions
diff --git a/examples/quantifiers.sol b/examples/quantifiers.sol
new file mode 100644
index 0000000..3a65145
--- /dev/null
+++ b/examples/quantifiers.sol
@@ -0,0 +1,40 @@
+% Universals over infinite domains are proven or refuted
+% symbolically, never enumerated.
+
+% The specification's true example: every natural is at least zero.
+Query expression:
+  [ForAll variable: X
+          quantifier: [Natural value: X]
+          body: [GreaterEqual left: X right: 0]]
+
+% The specification's false example: not every integer is.
+Query expression:
+  [ForAll variable: X
+          quantifier: [Integer value: X]
+          body: [GreaterEqual left: X right: 0]]
+
+% Subtype inclusion, decided symbolically: every integer is a
+% rational, literally.
+Query expression:
+  [ForAll variable: X
+          quantifier: [Integer value: X]
+          body: [Rational value: X]]
+
+% The algebra of Plus: adding zero is the identity, over all
+% integers, stated flat as membership.
+Query expression:
+  [ForAll variable: X
+          quantifier: [Integer value: X]
+          body: [Plus left: X right: 0 result: X]]
+
+% Universals over finite quantifiers just run.
+Query expression:
+  [ForAll variable: X
+          quantifier: [Between value: X lower: 1 upper: 5]
+          body: [GreaterThan left: X right: 0]]
+
+% Existence, over a finite quantifier.
+Query expression:
+  [Exists variable: X
+          quantifier: [Between value: X lower: 1 upper: 10]
+          body: [Times left: X right: X result: 49]]