pseudo-tests-and-callp

(in-package "ACL2")

(define pseudo-tests-and-callp
  (x)
  :returns (yes/no booleanp)
  :parents (std/system)
  :short "Recognize well-formed @('tests-and-call') records."
  :long (topstring (p "A @('tests-and-call') record is defined as")
    (codeblock "(defrec tests-and-call (tests call) nil)")
    (p "(see the ACL2 source code).")
    (p "In a well-formed @('tests-and-call') record,
     @('tests') must be a list of terms and
     @('call') must be a term.")
    (p "This recognizer is analogous to @(tsee pseudo-tests-and-callsp)."))
  (case-match x
    (('tests-and-call tests call) (and (pseudo-term-listp tests) (pseudo-termp call)))
    (& nil))
  ///
  (defthm weak-tests-and-call-p-when-pseudo-tests-and-callp
    (implies (pseudo-tests-and-callp x)
      (weak-tests-and-call-p x))))