Major Section: THEORIES

When you disable the definition or executable-counterpart of a built-in function, you may see a warning, for example as follows.

ACL2 !>(in-theory (disable mv-nth)) ACL2 Warning [Theory] in ( IN-THEORY (DISABLE ...)): Although the theory expression (DISABLE MV-NTH) disables the :DEFINITION rule for MV-NTH, some expansions involving this function may still occur. See :DOC theories-and-primitives.

This warning can be eliminated by turning off all theory warnings (see set-inhibit-warnings) or simply by evaluating the following form.

(assign verbose-theory-warning nil)But before you eliminate such warnings, you may wish to read the following to understand their significance.

First consider the following example, evaluated after the `in-theory`

event displayed above.

ACL2 !>(thm (equal (mv-nth 2 (list a b c d e)) c)) Q.E.D. Summary Form: ( THM ...) Rules: ((:DEFINITION MV-NTH) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 19 Proof succeeded. ACL2 !>

Note that even though the definition of `mv-nth`

had been
disabled, nevertheless its definition rule was used in proving this
theorem. It is as though `mv-nth`

had not been been disabled after all!
The warning is intended to indicate that expansion of `mv-nth`

calls may be
made by the theorem prover even when `mv-nth`

is disabled. Indeed, the
prover has special-purpose code for simplifying certain `mv-nth`

calls.

A similar issue can arise for `executable-counterpart`

rules, as the
following log illustrates.

ACL2 !>(in-theory (disable (:executable-counterpart symbolp))) ACL2 Warning [Theory] in ( IN-THEORY (DISABLE ...)): Although the theory expression (DISABLE (:EXECUTABLE-COUNTERPART SYMBOLP)) disables the :EXECUTABLE-COUNTERPART rule for SYMBOLP, some calls involving this function may still be made. See :DOC theories-and-primitives. Summary Form: ( IN-THEORY (DISABLE ...)) Rules: NIL Warnings: Theory Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) 2921 ACL2 !>(thm (symbolp 'a)) Q.E.D. Summary Form: ( THM ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Proof succeeded. ACL2 !>

In general, ACL2 warns when `in-theory`

events or hints leave
you in a theory where a rule for a built-in function is disabled but may be
applied in some cases nonetheless, because of special-purpose prover code for
handling calls of that function. The built-in function symbols with such
definition rules or executable-counterpart rules are those in the
following two lists, respectively.

ACL2 !>*definition-minimal-theory* (MV-NTH IFF NOT IMPLIES EQ ATOM EQL = /= NULL ENDP ZEROP SYNP PLUSP MINUSP LISTP RETURN-LAST MV-LIST THE-ERROR WORMHOLE-EVAL FORCE CASE-SPLIT DOUBLE-REWRITE) ACL2 !>*built-in-executable-counterparts* (ACL2-NUMBERP BINARY-* BINARY-+ UNARY-- UNARY-/ < CAR CDR CHAR-CODE CHARACTERP CODE-CHAR COMPLEX COMPLEX-RATIONALP COERCE CONS CONSP DENOMINATOR EQUAL IF IMAGPART INTEGERP INTERN-IN-PACKAGE-OF-SYMBOL NUMERATOR PKG-WITNESS PKG-IMPORTS RATIONALP REALPART STRINGP SYMBOL-NAME SYMBOL-PACKAGE-NAME SYMBOLP NOT) ACL2 !>