Term-table
A table used to validate meta rules
Example:
(table term-table t '((binary-+ x y) '3 'nil (car x)))
See table for a general discussion of tables and the table
event used to manipulate tables.
The ``term-table'' is used at the time a meta rule is checked for
syntactic correctness. Each proposed metafunction is run on each term in this
table, and the result in each case is checked to make sure that it is a
termp in the current world. In each case where this test fails, a
warning is printed.
By default, when a metafunction is run in support of the application of a
meta rule, the result must be a term (see termp) in the current world.
When the result is not a term, a hard error arises. (However, see the last
paragraph below.) The term-table is simply a means for providing
feedback to the user at the time a meta rule is submitted, warning of the
definite possibility that such a hard error will occur at some point in the
future.
The key used in term-table is arbitrary. The top-most value is always
the one that is used; it is the entire list of terms to be considered. Each
must be a termp in the current ACL2 world.
The runtime check on the output of metafunctions can be avoided by proving
that it will always succeed (see well-formedness-guarantee) or by
telling ACL2 to skip the test at the risk of soundness (see set-skip-meta-termp-checks).
