		Search-engine friendly clone of the ACL2 documentation.

Schar-format

Schar-formatp

Recognizer for schar-format structures.

Signature
(schar-formatp x) → *

Definitions and Theorems

Function: schar-formatp

(defun schar-formatp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'schar-formatp))
    (declare (ignorable __function__))
    (and (mbe :logic (and (alistp x)
                          (equal (strip-cars x) '(signed trap)))
              :exec (fty::alist-with-carsp x '(signed trap)))
         (b* ((signed (cdr (std::da-nth 0 x)))
              (trap (cdr (std::da-nth 1 x))))
           (and (signed-formatp signed)
                (booleanp trap))))))

Theorem: consp-when-schar-formatp

(defthm consp-when-schar-formatp
  (implies (schar-formatp x) (consp x))
  :rule-classes :compound-recognizer)