		Search-engine friendly clone of the ACL2 documentation.

Macro-info-object

Make-macro-info-object

Basic constructor macro for macro-info-object structures.

Syntax

(make-macro-info-object [:replace <replace>])

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

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

Definition

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

Macro: make-macro-info-object

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

Function: macro-info-object

(defun macro-info-object (replace)
  (declare (xargs :guard (plexeme-listp replace)))
  (declare (xargs :guard (plexeme-list-token/space-p replace)))
  (b* ((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 :object (list replace)))))