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
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
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-CHECK 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 !>