|
|
|---|
|
|
|
|---|
Routines for simplifying terms.
NOTE: If you are looking for a simple interface to the ACL2 rewriter, see rewrite$.
The routines provided by the expander can be useful in generating theorems and simplifying expressions, under given assumptions.
They were developed rather in a hurry and should be used without expecting the usual standards of care present in development of ACL2 code. Once these routines are used to generate theorems for you, you should check the theorems directly with ACL2.
To load the expander, run:
(include-book "misc/expander" :dir :system)