		Search-engine friendly clone of the ACL2 documentation.

Macro-info-function

Make-macro-info-function

Basic constructor macro for macro-info-function structures.

Syntax

(make-macro-info-function [:params <params>] 
                          [:ellipsis <ellipsis>] 
                          [:replace <replace>])

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

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

Definition

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

Macro: make-macro-info-function

(defmacro make-macro-info-function (&rest args)
  (std::make-aggregate 'macro-info-function
                       args '((:params) (:ellipsis) (:replace))
                       'make-macro-info-function
                       nil))

Function: macro-info-function

(defun macro-info-function (params ellipsis replace)
  (declare (xargs :guard (and (ident-listp params)
                              (booleanp ellipsis)
                              (plexeme-listp replace))))
  (declare (xargs :guard (plexeme-list-token/space-p replace)))
  (b* ((params (mbe :logic (ident-list-fix params)
                    :exec params))
       (ellipsis (mbe :logic (bool-fix ellipsis)
                      :exec ellipsis))
       (replace (mbe :logic (plexeme-list-fix replace)
                     :exec replace)))
    (let ((replace (mbe :logic
                        (if (plexeme-list-token/space-p replace)
                            replace
                          nil)
                        :exec replace)))
      (cons :function (list params ellipsis replace)))))