		Search-engine friendly clone of the ACL2 documentation.

Observability-config

Observability-config-p

Recognizer for observability-config structures.

Signature
(observability-config-p x) → *

Definitions and Theorems

Function: observability-config-p

(defun observability-config-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'observability-config-p))
  (declare (ignorable __function__))
  (and
   (consp x)
   (eq (car x) :observability-config)
   (mbe
     :logic
     (and (alistp (cdr x))
          (equal (strip-cars (cdr x))
                 '(hyp-max-size concl-min-size min-ratio gatesimp)))
     :exec (fty::alist-with-carsp
                (cdr x)
                '(hyp-max-size concl-min-size min-ratio gatesimp)))
   (b* ((hyp-max-size (cdr (std::da-nth 0 (cdr x))))
        (concl-min-size (cdr (std::da-nth 1 (cdr x))))
        (min-ratio (cdr (std::da-nth 2 (cdr x))))
        (gatesimp (cdr (std::da-nth 3 (cdr x)))))
     (and (acl2::maybe-natp hyp-max-size)
          (acl2::maybe-natp concl-min-size)
          (rationalp min-ratio)
          (gatesimp-p gatesimp))))))

Theorem: consp-when-observability-config-p

(defthm consp-when-observability-config-p
  (implies (observability-config-p x)
           (consp x))
  :rule-classes :compound-recognizer)