		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Macro-lookup

Look up a macro in a macro table.

Signature
(macro-lookup name table) → info?
Arguments: name — Guard (identp name).; table — Guard (macro-tablep table).
Returns: info? — Type (macro-info-optionp info?).

We return nil if the macro is not in the table.

Definitions and Theorems

Function: macro-lookup

(defun macro-lookup (name table)
  (declare (xargs :guard (and (identp name)
                              (macro-tablep table))))
  (cdr (assoc-equal (ident-fix name)
                    (macro-table->alist table))))

Theorem: macro-info-optionp-of-macro-lookup

(defthm macro-info-optionp-of-macro-lookup
  (b* ((info? (macro-lookup name table)))
    (macro-info-optionp info?))
  :rule-classes :rewrite)

Theorem: macro-lookup-of-ident-fix-name

(defthm macro-lookup-of-ident-fix-name
  (equal (macro-lookup (ident-fix name) table)
         (macro-lookup name table)))

Theorem: macro-lookup-ident-equiv-congruence-on-name

(defthm macro-lookup-ident-equiv-congruence-on-name
  (implies (ident-equiv name name-equiv)
           (equal (macro-lookup name table)
                  (macro-lookup name-equiv table)))
  :rule-classes :congruence)

Theorem: macro-lookup-of-macro-table-fix-table

(defthm macro-lookup-of-macro-table-fix-table
  (equal (macro-lookup name (macro-table-fix table))
         (macro-lookup name table)))

Theorem: macro-lookup-macro-table-equiv-congruence-on-table

(defthm macro-lookup-macro-table-equiv-congruence-on-table
  (implies (macro-table-equiv table table-equiv)
           (equal (macro-lookup name table)
                  (macro-lookup name table-equiv)))
  :rule-classes :congruence)