aboutsummaryrefslogtreecommitdiffstats
path: root/README.org
diff options
context:
space:
mode:
Diffstat (limited to 'README.org')
-rw-r--r--README.org5
1 files changed, 4 insertions, 1 deletions
diff --git a/README.org b/README.org
index cd6149c..832ce9d 100644
--- a/README.org
+++ b/README.org
@@ -191,7 +191,10 @@ algebra.
Build with =nix develop -c dune build=; run the tests with =nix
develop -c dune runtest=; run a program with =dune exec sol --
-file.sol=.
+file.sol=. Worked examples live in =examples/= (see
+=examples/README.org=); machine checked proofs in =theories/=
+(structural and lexicographic decrease, extracted into admission;
+the interval characterizations behind propagation).
Machine checked proofs live in =theories/=: the admission checker's
core claim, that strict containment decreases a well founded