Some noteworthy clause-processors include:
- Basically like defevaluator but faster when you have a lot of
functions in your evaluator.
- The def-join-thms macro adds theorems about conjoin, disjoin, etc for
- The def-unify macro proves a unify/substitution algorithm correct for
- The def-meta-extract macro sets up support for using the meta-extract stuff to assume facts from the world are correct.
- Implements a beta-reduction function, proves it preserves pseudo-termp, and
provides a macro for proving correctness of beta-reduction for your
- 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.
- A verified clause-processor and customized rewriter for large terms
that uses existing ACL2 rewrite rules to prove theorems.