		Search-engine friendly clone of the ACL2 documentation.

Function-header

Make-function-header

Basic constructor macro for function-header structures.

Syntax

(make-function-header [:name <name>] 
                      [:inputs <inputs>] 
                      [:outputs <outputs>])

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

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

Definition

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

Macro: make-function-header

(defmacro make-function-header (&rest args)
  (std::make-aggregate 'function-header
                       args '((:name) (:inputs) (:outputs))
                       'make-function-header
                       nil))

Function: function-header

(defun function-header (name inputs outputs)
  (declare (xargs :guard (and (identifierp name)
                              (typed-variable-listp inputs)
                              (typed-variable-listp outputs))))
  (declare (xargs :guard t))
  (let ((__function__ 'function-header))
    (declare (ignorable __function__))
    (b* ((name (mbe :logic (identifier-fix name)
                    :exec name))
         (inputs (mbe :logic (typed-variable-list-fix inputs)
                      :exec inputs))
         (outputs (mbe :logic (typed-variable-list-fix outputs)
                       :exec outputs)))
      (list (cons 'name name)
            (cons 'inputs inputs)
            (cons 'outputs outputs)))))