1 files changed, 52 insertions, 0 deletions
diff --git a/examples/README.org b/examples/README.org
new file mode 100644
index 0000000..20b853a
--- /dev/null
+++ b/examples/README.org
@@ -0,0 +1,52 @@
+#+TITLE: Sol Examples
+
+* Running
+
+From the repository root, with Nix:
+
+#+BEGIN_SRC sh
+nix develop -c dune exec sol -- examples/family.sol
+#+END_SRC
+
+Or enter the shell once and run them all:
+
+#+BEGIN_SRC sh
+nix develop
+dune build
+for f in examples/*.sol; do echo "== $f"; dune exec sol -- "$f"; done
+#+END_SRC
+
+Without a file argument, =dune exec sol= starts a REPL: declarations
+accumulate, =Query expression: ...= runs immediately, one statement
+per line.
+
+* The files
+
+- =family.sol= :: relations, facts, a rule, joins through shared
+  variables, decidable denial with =:not=, and the =World= scoped
+  negation form.
+- =arithmetic.sol= :: =Plus= and =Times= evaluating forward and
+  solving backward through the rationals; minimal shape, where
+  =1/2 + 1/2= is the integer =1=.
+- =recursion.sol= :: structural recursion admitted by the decrease
+  checker extracted from Rocq, and Even/Odd mutual recursion under a
+  lexicographic measure.
+- =constraints.sol= :: membership is not generation: residuation,
+  interval propagation, finite ranges enumerating, contradictions
+  answering no, and explicit bounded generation with =Between=.
+- =quantifiers.sol= :: universals over infinite domains proven or
+  refuted symbolically, including the specification's own true and
+  false examples and the =Plus= identity; finite quantifiers simply
+  run.
+- =integrity.sol= :: schemas as membership: primitive domains, a
+  refinement, and a foreign key as a criterion. The comments at the
+  bottom show facts that make admission reject the whole program;
+  uncomment one and run again to see it happen.
+
+* Reading the answers
+
+Each query prints one line per answer: variable bindings in Sol
+notation, =yes.= for a closed query that holds, =no.= for one that
+does not. An answer conditioned on open membership prints its
+residual constraints after the bindings, as the propositions they
+are.