		Search-engine friendly clone of the ACL2 documentation.

Syndef::acid4

Syndef::acid4-P

Recognizer for syndef::acid4 structures.

Signature
(syndef::|acid4-P| syndef::x) → *

Definitions and Theorems

Function: acid4-p

(defun syndef::|acid4-P| (syndef::x)
  (declare (xargs :guard t))
  (let ((__function__ 'syndef::|acid4-P|))
    (declare (ignorable __function__))
    (and (consp syndef::x)
         (eq (car syndef::x) :|acid4|)
         (mbe :logic (and (alistp (cdr syndef::x))
                          (equal (strip-cars (cdr syndef::x))
                                 '(syndef::|id|)))
              :exec (fty::alist-with-carsp (cdr syndef::x)
                                           '(syndef::|id|)))
         (b* ((syndef::|id| (cdr (std::da-nth 0 (cdr syndef::x)))))
           (integerp syndef::|id|)))))

Theorem: consp-when-acid4-p

(defthm syndef::|CONSP-WHEN-acid4-P|
  (implies (syndef::|acid4-P| syndef::x)
           (consp syndef::x))
  :rule-classes :compound-recognizer)