		Search-engine friendly clone of the ACL2 documentation.

Fun-sinfo

Fun-sinfop

Recognizer for fun-sinfo structures.

Signature
(fun-sinfop x) → *

Definitions and Theorems

Function: fun-sinfop

(defun fun-sinfop (x)
 (declare (xargs :guard t))
 (let ((__function__ 'fun-sinfop))
  (declare (ignorable __function__))
  (and
     (mbe :logic (and (alistp x)
                      (equal (strip-cars x)
                             '(inputs output definedp)))
          :exec (fty::alist-with-carsp x '(inputs output definedp)))
     (b* ((inputs (cdr (std::da-nth 0 x)))
          (output (cdr (std::da-nth 1 x)))
          (definedp (cdr (std::da-nth 2 x))))
       (and (type-listp inputs)
            (typep output)
            (booleanp definedp))))))

Theorem: consp-when-fun-sinfop

(defthm consp-when-fun-sinfop
  (implies (fun-sinfop x) (consp x))
  :rule-classes :compound-recognizer)