• Top

• Fundecl

Fundeclp

Recognizer for fundecl structures.

Signature

(fundeclp x) → *

Definitions and Theorems

Function: fundeclp

(defun fundeclp (x)
 (declare (xargs :guard t))
 (let ((__function__ 'fundeclp))
  (declare (ignorable __function__))
  (and
   (consp x)
   (eq (car x) :fundecl)
   (mbe
      :logic
      (and (alistp (cdr x))
           (equal (strip-cars (cdr x))
                  '(annotations sort
                                name inputs output body finalizer)))
      :exec (fty::alist-with-carsp
                 (cdr x)
                 '(annotations sort
                               name inputs output body finalizer)))
   (b* ((annotations (cdr (std::da-nth 0 (cdr x))))
        (sort (cdr (std::da-nth 1 (cdr x))))
        (name (cdr (std::da-nth 2 (cdr x))))
        (inputs (cdr (std::da-nth 3 (cdr x))))
        (output (cdr (std::da-nth 4 (cdr x))))
        (body (cdr (std::da-nth 5 (cdr x))))
        (finalizer (cdr (std::da-nth 6 (cdr x)))))
     (and (annotation-listp annotations)
          (fun-sortp sort)
          (identifierp name)
          (funparam-listp inputs)
          (typep output)
          (statement-listp body)
          (finalizer-optionp finalizer))))))

Theorem: consp-when-fundeclp

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