Basic constructor macro for atj-function-type structures.
(make-atj-function-type [:inputs <inputs>] [:outputs <outputs>] [:arrays <arrays>])
This is the usual way to construct atj-function-type structures. It simply conses together a structure with the specified fields.
This macro generates a new atj-function-type structure from scratch. See also change-atj-function-type, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-atj-function-type (&rest args) (std::make-aggregate 'atj-function-type args '((:inputs) (:outputs) (:arrays)) 'make-atj-function-type nil))
Function:
(defun atj-function-type (inputs outputs arrays) (declare (xargs :guard (and (atj-type-listp inputs) (atj-type-listp outputs) (symbol-listp arrays)))) (declare (xargs :guard t)) (let ((__function__ 'atj-function-type)) (declare (ignorable __function__)) (b* ((inputs (mbe :logic (atj-type-list-fix inputs) :exec inputs)) (outputs (mbe :logic (atj-type-list-fix outputs) :exec outputs)) (arrays (mbe :logic (acl2::symbol-list-fix arrays) :exec arrays))) (list inputs outputs arrays))))