		Search-engine friendly clone of the ACL2 documentation.

Atc-event-and-code-generation

Test*

Wrapper for contextual tests.

Signature
(test* x) → *

In atc-contextualize, we wrap tests from the context premises with this identity function, to prevent ACL2 from making use of them, in the generated modular theorems, to simplify things in ways that interfere with the compositional proofs. For instance, when ACL2 has a hypothesis (not <term>) in context, it rewrites occurrences of <term> with nil: this is generally good for interactive proofs, but not if that prevents a previously proved theorem from applying, about a subterm that is supposed not to be simplified.

Definitions and Theorems

Function: test*

(defun test* (x)
  (declare (xargs :guard t))
  (let ((__function__ 'test*))
    (declare (ignorable __function__))
    x))

Theorem: test*-of-t

(defthm test*-of-t (test* t))