WARNING: Use of this macro may render ACL2 unsound, which is why it requires a trust tag. If you obtained an error during application of a metafunction, a hypothesis metafunction, or a clause-processor, it might well be best to rewrite that function to avoid generating terms with the ``forbidden'' function calls described in that error message. However, judicious use of this macro can be useful during development; the rest of this topic describes its usage.
The result of applying a metafunction (or a hypothesis metafunction) must be a term. Similarly, the result of applying a clause-processor must be a list of clauses, where a clause is a list of terms (see clause). If these conditions fail, then an error occurs; see term-table for how one obtains some assistance towards avoiding such errors.
By default, ACL2 actually enforces a stronger requirement: the resulting
term or clause-list cannot contain any calls of ``forbidden'' function
symbols: ones that would be illegal when submitting a theorem. These include
function symbols that are untouchable (see remove-untouchable)
as well as those that are keys of the alist
These two checks — that the results are terms and that they contain
no calls of forbidden function symbols — can be expensive for large
terms. The macro
There are two legal ways to call this macro, as follows. Note that the arguments are not evaluated.
; Skip all such checks: (set-skip-meta-termp-checks t) ; Skip such checks for functions fn1, ..., fnk (each of which is presumably a ; metafunction, hypothesis metafunction, or clause-processor): (set-skip-meta-termp-checks (fn1 ... fnk))
A special case of the second form above is to perform all such checks:
This macro actually generates a local table event, for the
ACL2 !>:trans1 (set-skip-meta-termp-checks (f g)) (LOCAL (SET-SKIP-META-TERMP-CHECKS! (F G))) ACL2 !>:trans1 (set-skip-meta-termp-checks! (f g)) (TABLE SKIP-META-TERMP-CHECKS-TABLE T '(F G)) ACL2 !>
It is probably good practice to use