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.
Major Section: EVENTS
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.
Whenever a metafunction is run in support of the application of a
meta rule, the result must be a term in the current world. When the
result is not a term, a hard error arises. 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.