		Search-engine friendly clone of the ACL2 documentation.

Function-definition

Function-definitionp

Recognizer for function-definition structures.

Signature
(function-definitionp x) → *

Definitions and Theorems

Function: function-definitionp

(defun function-definitionp (x)
 (declare (xargs :guard t))
 (let ((__function__ 'function-definitionp))
  (declare (ignorable __function__))
  (and
     (mbe :logic
          (and (alistp x)
               (equal (strip-cars x)
                      '(header precondition postcondition definer)))
          :exec (fty::alist-with-carsp
                     x
                     '(header precondition postcondition definer)))
     (b* ((header (cdr (std::da-nth 0 x)))
          (precondition (cdr (std::da-nth 1 x)))
          (postcondition (cdr (std::da-nth 2 x)))
          (definer (cdr (std::da-nth 3 x))))
       (and (function-headerp header)
            (maybe-expressionp precondition)
            (maybe-expressionp postcondition)
            (function-definerp definer))))))

Theorem: consp-when-function-definitionp

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