		Search-engine friendly clone of the ACL2 documentation.

Macro-table

Make-macro-table

Basic constructor macro for macro-table structures.

Syntax

(make-macro-table [:alist <alist>])

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

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

Definition

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

Macro: make-macro-table

(defmacro make-macro-table (&rest args)
  (std::make-aggregate 'macro-table
                       args '((:alist))
                       'make-macro-table
                       nil))

Function: macro-table

(defun macro-table (alist)
  (declare (xargs :guard (ident-macroinfo-alistp alist)))
  (declare (xargs :guard (no-duplicatesp-equal (strip-cars alist))))
  (b* ((alist (mbe :logic (ident-macroinfo-alist-fix alist)
                   :exec alist)))
    (let ((alist (mbe :logic
                      (if (no-duplicatesp-equal (strip-cars alist))
                          alist
                        nil)
                      :exec alist)))
      (list (cons 'alist alist)))))