		Search-engine friendly clone of the ACL2 documentation.

Types

Type-fpconvert

Convert function types to pointer types.

Signature
(type-fpconvert type) → new-type
Arguments: type — Guard (typep type).
Returns: new-type — Type (typep new-type).

This performs the conversion in [C17:6.3.2.1/4]. It leaves non-function types unchanged.

Definitions and Theorems

Function: type-fpconvert

(defun type-fpconvert (type)
  (declare (xargs :guard (typep type)))
  (if (type-case type :function)
      (make-type-pointer :to (type-fix type))
    (type-fix type)))

Theorem: typep-of-type-fpconvert

(defthm typep-of-type-fpconvert
  (b* ((new-type (type-fpconvert type)))
    (typep new-type))
  :rule-classes :rewrite)

Theorem: type-fpconvert-of-type-fix-type

(defthm type-fpconvert-of-type-fix-type
  (equal (type-fpconvert (type-fix type))
         (type-fpconvert type)))

Theorem: type-fpconvert-type-equiv-congruence-on-type

(defthm type-fpconvert-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (type-fpconvert type)
                  (type-fpconvert type-equiv)))
  :rule-classes :congruence)