		Search-engine friendly clone of the ACL2 documentation.

Std/system

Pseudo-tests-and-callp

Recognize well-formed tests-and-call records.

Signature
(pseudo-tests-and-callp x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

A tests-and-call record is defined as

(defrec tests-and-call (tests call) nil)

(see the ACL2 source code).

In a well-formed tests-and-call record, tests must be a list of terms and call must be a term.

This recognizer is analogous to pseudo-tests-and-callsp.

Definitions and Theorems

Function: pseudo-tests-and-callp

(defun pseudo-tests-and-callp (x)
       (declare (xargs :guard t))
       (let ((__function__ 'pseudo-tests-and-callp))
            (declare (ignorable __function__))
            (case-match x
                        (('tests-and-call tests call)
                         (and (pseudo-term-listp tests)
                              (pseudo-termp call)))
                        (& nil))))

Theorem: booleanp-of-pseudo-tests-and-callp

(defthm booleanp-of-pseudo-tests-and-callp
        (b* ((yes/no (pseudo-tests-and-callp x)))
            (booleanp yes/no))
        :rule-classes :rewrite)

Theorem: weak-tests-and-call-p-when-pseudo-tests-and-callp

(defthm weak-tests-and-call-p-when-pseudo-tests-and-callp
        (implies (pseudo-tests-and-callp x)
                 (weak-tests-and-call-p x)))