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

Theorem: consp-when-fundefp

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