Clause-processor-tools
Noteworthy clause-processors
Some noteworthy clause-processors include:
- tools/defevaluator-fast
- Basically like defevaluator but faster when you have a lot of
functions in your evaluator.
- clause-processor/join-thms
- The def-join-thms macro adds theorems about conjoin, disjoin, etc for
your evaluator.
- clause-processors/unify-subst
- The def-unify macro proves a unify/substitution algorithm correct for
your evaluator.
- clause-processors/meta-extract-user
- The def-meta-extract macro sets up support for using the meta-extract stuff to assume facts from the world are correct.
- misc/beta-reduce
- Implements a beta-reduction function, proves it preserves pseudo-termp, and
provides a macro for proving correctness of beta-reduction for your
evaluator.
- centaur/misc/beta-reduce-full
- Implements a recursive beta-reducer to expand away all lambdas, proves it
preserves pseudo-termp, proves it is correct for an evaluator.
See also the clause-processors directory in general; many books are
documented only in comments.
Subtopics
- Rp-rewriter
- A verified clause-processor and customized rewriter for large terms
that uses existing ACL2 rewrite rules to prove theorems.
