		Search-engine friendly clone of the ACL2 documentation.

Fundef

Fundefp

Recognizer for fundef structures.

Signature
(fundefp x) → *

Definitions and Theorems

Function: fundefp

(defun fundefp (x)
 (declare (xargs :guard t))
 (let ((__function__ 'fundefp))
  (declare (ignorable __function__))
  (and
   (mbe
      :logic
      (and (alistp x)
           (equal (strip-cars x)
                  '(extension spec declor asm? attribs decls body)))
      :exec (fty::alist-with-carsp
                 x
                 '(extension spec declor asm? attribs decls body)))
   (b* ((extension (cdr (std::da-nth 0 x)))
        (spec (cdr (std::da-nth 1 x)))
        (declor (cdr (std::da-nth 2 x)))
        (asm? (cdr (std::da-nth 3 x)))
        (attribs (cdr (std::da-nth 4 x)))
        (decls (cdr (std::da-nth 5 x)))
        (body (cdr (std::da-nth 6 x))))
     (and (booleanp extension)
          (decl-spec-listp spec)
          (declorp declor)
          (asm-name-spec-optionp asm?)
          (attrib-spec-listp attribs)
          (decl-listp decls)
          (stmtp body))))))

Theorem: consp-when-fundefp

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