TERM-TABLE

a table used to validate meta rules
Major Section:  SWITCHES-PARAMETERS-AND-MODES-OH-MY

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.