Paco
Paco is a cut-down, simplified ACL2-like theorem prover for
pedagogical use.
The ACL2 source files for paco are located in projects/paco.
These files can be built by running, e.g., make paco from the books/
directory. After building these source files, to run paco on some examples,
you may go to the directory projects/paco/books and run:
(ld "proveall.lsp" :ld-pre-eval-print t)
For copyright and license information, see
books/projects/paco/LICENSE.
