		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Funinfo-for-fundef

Function information for a function definition.

Signature
(funinfo-for-fundef fundef) → funinfo
Arguments: fundef — Guard (fundefp fundef).
Returns: funinfo — Type (funinfop funinfo).

This just takes the inputs, outputs, and body of the function definition and forms function information with them.

Definitions and Theorems

Function: funinfo-for-fundef

(defun funinfo-for-fundef (fundef)
  (declare (xargs :guard (fundefp fundef)))
  (let ((__function__ 'funinfo-for-fundef))
    (declare (ignorable __function__))
    (make-funinfo :inputs (fundef->inputs fundef)
                  :outputs (fundef->outputs fundef)
                  :body (fundef->body fundef))))

Theorem: funinfop-of-funinfo-for-fundef

(defthm funinfop-of-funinfo-for-fundef
  (b* ((funinfo (funinfo-for-fundef fundef)))
    (funinfop funinfo))
  :rule-classes :rewrite)

Theorem: funinfo-for-fundef-of-fundef-fix-fundef

(defthm funinfo-for-fundef-of-fundef-fix-fundef
  (equal (funinfo-for-fundef (fundef-fix fundef))
         (funinfo-for-fundef fundef)))

Theorem: funinfo-for-fundef-fundef-equiv-congruence-on-fundef

(defthm funinfo-for-fundef-fundef-equiv-congruence-on-fundef
  (implies (fundef-equiv fundef fundef-equiv)
           (equal (funinfo-for-fundef fundef)
                  (funinfo-for-fundef fundef-equiv)))
  :rule-classes :congruence)