		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Macro-table-init

Initial macro table.

Signature
(macro-table-init) → table
Returns: table — Type (macro-tablep table).

This is the table at the beginning of a file to preprocess. For now this is empty, but we must extend it with the necessary predefined macros [C17:6.10.8], which in general depend on the implementation environment.

Definitions and Theorems

Function: macro-table-init

(defun macro-table-init nil
  (declare (xargs :guard t))
  (macro-table nil))

Theorem: macro-tablep-of-macro-table-init

(defthm macro-tablep-of-macro-table-init
  (b* ((table (macro-table-init)))
    (macro-tablep table))
  :rule-classes :rewrite)