#+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.