		Search-engine friendly clone of the ACL2 documentation.

Static-soundness

Funinfo-to-funtype

Turn function information into a function type.

Signature
(funinfo-to-funtype funinfo) → ftype
Arguments: funinfo — Guard (funinfop funinfo).
Returns: ftype — Type (funtypep ftype).

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.

Definitions and Theorems

Function: funinfo-to-funtype

(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: funtypep-of-funinfo-to-funtype

(defthm funtypep-of-funinfo-to-funtype
        (b* ((ftype (funinfo-to-funtype funinfo)))
            (funtypep ftype))
        :rule-classes :rewrite)

Theorem: len-of-funinfo->inputs

(defthm len-of-funinfo->inputs
        (equal (len (funinfo->inputs funinfo))
               (funtype->in (funinfo-to-funtype funinfo))))

Theorem: len-of-funinfo->outputs

(defthm len-of-funinfo->outputs
        (equal (len (funinfo->outputs funinfo))
               (funtype->out (funinfo-to-funtype funinfo))))

Theorem: funinfo-to-funtype-of-funinfo-fix-funinfo

(defthm funinfo-to-funtype-of-funinfo-fix-funinfo
        (equal (funinfo-to-funtype (funinfo-fix funinfo))
               (funinfo-to-funtype funinfo)))

Theorem: funinfo-to-funtype-funinfo-equiv-congruence-on-funinfo

(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)