		Search-engine friendly clone of the ACL2 documentation.

Atc-fn-info

Atc-fn-infop

Recognizer for atc-fn-info structures.

Signature
(atc-fn-infop x) → *

Definitions and Theorems

Function: atc-fn-infop

(defun atc-fn-infop (x)
 (declare (xargs :guard t))
 (let ((__function__ 'atc-fn-infop))
  (declare (ignorable __function__))
  (and
   (mbe :logic
        (and (alistp x)
             (equal (strip-cars x)
                    '(out-type in-types loop?
                               affect extobjs result-thm correct-thm
                               correct-mod-thm measure-nat-thm
                               fun-env-thm limit guard)))
        :exec (fty::alist-with-carsp
                   x
                   '(out-type in-types loop?
                              affect extobjs result-thm correct-thm
                              correct-mod-thm measure-nat-thm
                              fun-env-thm limit guard)))
   (b* ((out-type (cdr (std::da-nth 0 x)))
        (in-types (cdr (std::da-nth 1 x)))
        (loop? (cdr (std::da-nth 2 x)))
        (affect (cdr (std::da-nth 3 x)))
        (extobjs (cdr (std::da-nth 4 x)))
        (result-thm (cdr (std::da-nth 5 x)))
        (correct-thm (cdr (std::da-nth 6 x)))
        (correct-mod-thm (cdr (std::da-nth 7 x)))
        (measure-nat-thm (cdr (std::da-nth 8 x)))
        (fun-env-thm (cdr (std::da-nth 9 x)))
        (limit (cdr (std::da-nth 10 x)))
        (guard (cdr (std::da-nth 11 x))))
     (and (type-optionp out-type)
          (type-listp in-types)
          (stmt-optionp loop?)
          (symbol-listp affect)
          (symbol-listp extobjs)
          (symbolp result-thm)
          (symbolp correct-thm)
          (symbolp correct-mod-thm)
          (symbolp measure-nat-thm)
          (symbolp fun-env-thm)
          (pseudo-termp limit)
          (symbolp guard))))))

Theorem: consp-when-atc-fn-infop

(defthm consp-when-atc-fn-infop
  (implies (atc-fn-infop x) (consp x))
  :rule-classes :compound-recognizer)