Turn function information into a function type.
A function type is the static counterpart of function information. We extract the number of inputs and outputs from the function information's input and output lists.
Function:
(defun funinfo-to-funtype (funinfo) (declare (xargs :guard (funinfop funinfo))) (let ((__function__ 'funinfo-to-funtype)) (declare (ignorable __function__)) (b* (((funinfo funinfo) funinfo)) (make-funtype :in (len funinfo.inputs) :out (len funinfo.outputs)))))
Theorem:
(defthm funtypep-of-funinfo-to-funtype (b* ((ftype (funinfo-to-funtype funinfo))) (funtypep ftype)) :rule-classes :rewrite)
Theorem:
(defthm len-of-funinfo->inputs (equal (len (funinfo->inputs funinfo)) (funtype->in (funinfo-to-funtype funinfo))))
Theorem:
(defthm len-of-funinfo->outputs (equal (len (funinfo->outputs funinfo)) (funtype->out (funinfo-to-funtype funinfo))))
Theorem:
(defthm funinfo-to-funtype-of-funinfo-fix-funinfo (equal (funinfo-to-funtype (funinfo-fix funinfo)) (funinfo-to-funtype funinfo)))
Theorem:
(defthm funinfo-to-funtype-funinfo-equiv-congruence-on-funinfo (implies (funinfo-equiv funinfo funinfo-equiv) (equal (funinfo-to-funtype funinfo) (funinfo-to-funtype funinfo-equiv))) :rule-classes :congruence)