		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)))