		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))
  (and (consp x)
       (consp (car x))
       (consp (car (car x)))
       (consp (cdr (car x)))
       (consp (cdr x))
       (consp (car (cdr x)))
       (consp (cdr (cdr x)))
       (b* ((extension (car (car (car x))))
            (specs (cdr (car (car x))))
            (declor (car (cdr (car x))))
            (asm? (cdr (cdr (car x))))
            (attribs (car (car (cdr x))))
            (declons (cdr (car (cdr x))))
            (body (car (cdr (cdr x))))
            (info (cdr (cdr (cdr x)))))
         (and (booleanp extension)
              (decl-spec-listp specs)
              (declorp declor)
              (asm-name-spec-optionp asm?)
              (attrib-spec-listp attribs)
              (declon-listp declons)
              (comp-stmtp body)
              (acl2::any-p info)))))

Theorem: consp-when-fundefp

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