Function type for a function definition.
This is just the number of inputs and outputs of the function.
Function:
(defun funtype-for-fundef (fundef) (declare (xargs :guard (fundefp fundef))) (let ((__function__ 'funtype-for-fundef)) (declare (ignorable __function__)) (make-funtype :in (len (fundef->inputs fundef)) :out (len (fundef->outputs fundef)))))
Theorem:
(defthm funtypep-of-funtype-for-fundef (b* ((funtype (funtype-for-fundef fundef))) (funtypep funtype)) :rule-classes :rewrite)
Theorem:
(defthm funtype-for-fundef-of-fundef-fix-fundef (equal (funtype-for-fundef (fundef-fix fundef)) (funtype-for-fundef fundef)))
Theorem:
(defthm funtype-for-fundef-fundef-equiv-congruence-on-fundef (implies (fundef-equiv fundef fundef-equiv) (equal (funtype-for-fundef fundef) (funtype-for-fundef fundef-equiv))) :rule-classes :congruence)