		Search-engine friendly clone of the ACL2 documentation.

Function-definition

Function-definition->header

Get the header field from a function-definition.

Signature
(function-definition->header x) → header
Arguments: x — Guard (function-definitionp x).
Returns: header — Type (function-headerp header).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: function-definition->header$inline

(defun function-definition->header$inline (x)
  (declare (xargs :guard (function-definitionp x)))
  (declare (xargs :guard t))
  (let ((__function__ 'function-definition->header))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and t x)))
           (function-header-fix (cdr (std::da-nth 0 x))))
         :exec (cdr (std::da-nth 0 x)))))

Theorem: function-headerp-of-function-definition->header

(defthm function-headerp-of-function-definition->header
  (b* ((header (function-definition->header$inline x)))
    (function-headerp header))
  :rule-classes :rewrite)

Theorem: function-definition->header$inline-of-function-definition-fix-x

(defthm
    function-definition->header$inline-of-function-definition-fix-x
 (equal
    (function-definition->header$inline (function-definition-fix x))
    (function-definition->header$inline x)))

Theorem: function-definition->header$inline-function-definition-equiv-congruence-on-x

(defthm
 function-definition->header$inline-function-definition-equiv-congruence-on-x
 (implies (function-definition-equiv x x-equiv)
          (equal (function-definition->header$inline x)
                 (function-definition->header$inline x-equiv)))
 :rule-classes :congruence)