		Search-engine friendly clone of the ACL2 documentation.

Type-function

Make-type-function

Basic constructor macro for type-function structures.

Syntax

(make-type-function [:ret <ret>] 
                    [:params <params>])

This is the usual way to construct type-function structures. It simply conses together a structure with the specified fields.

This macro generates a new type-function structure from scratch. See also change-type-function, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-type-function

(defmacro make-type-function (&rest args)
  (std::make-aggregate 'type-function
                       args '((:ret) (:params))
                       'make-type-function
                       nil))

Function: type-function

(defun type-function (ret params)
  (declare (xargs :guard (and (typep ret)
                              (type-paramsp params))))
  (declare (xargs :guard t))
  (b* ((ret (mbe :logic (type-fix ret) :exec ret))
       (params (mbe :logic (type-params-fix params)
                    :exec params)))
    (cons :function (cons ret params))))