		Search-engine friendly clone of the ACL2 documentation.

Function-environments

Fun-info-from-fundef

Create information for a function definition.

Signature
(fun-info-from-fundef fundef) → finfo
Arguments: fundef — Guard (fundefp fundef).
Returns: finfo — Type (fun-infop finfo).

Definitions and Theorems

Function: fun-info-from-fundef

(defun fun-info-from-fundef (fundef)
  (declare (xargs :guard (fundefp fundef)))
  (let ((__function__ 'fun-info-from-fundef))
    (declare (ignorable __function__))
    (b* (((fundef fundef) fundef)
         ((mv & params tyname)
          (tyspec+declor-to-ident+params+tyname
               fundef.tyspec fundef.declor)))
      (make-fun-info :params params
                     :result tyname
                     :body fundef.body))))

Theorem: fun-infop-of-fun-info-from-fundef

(defthm fun-infop-of-fun-info-from-fundef
  (b* ((finfo (fun-info-from-fundef fundef)))
    (fun-infop finfo))
  :rule-classes :rewrite)

Theorem: fun-info-from-fundef-of-fundef-fix-fundef

(defthm fun-info-from-fundef-of-fundef-fix-fundef
  (equal (fun-info-from-fundef (fundef-fix fundef))
         (fun-info-from-fundef fundef)))

Theorem: fun-info-from-fundef-fundef-equiv-congruence-on-fundef

(defthm fun-info-from-fundef-fundef-equiv-congruence-on-fundef
  (implies (fundef-equiv fundef fundef-equiv)
           (equal (fun-info-from-fundef fundef)
                  (fun-info-from-fundef fundef-equiv)))
  :rule-classes :congruence)