		Search-engine friendly clone of the ACL2 documentation.

Std/system/macro-queries

Macro-args+

Enhanced variant of macro-args.

Signature
(macro-args+ mac wrld) → result
Arguments: mac — Guard (symbolp mac).; wrld — Guard (plist-worldp wrld).
Returns: result — Type (true-listp result).

This returns the same result as macro-args, but it has a run-time check (which should always succeed) on the result that allows us to prove the return type theorem without strengthening the guard on wrld. Furthermore, this utility causes an error if called on a symbol that does not name a macro.

Definitions and Theorems

Function: macro-args+

(defun
 macro-args+ (mac wrld)
 (declare (xargs :guard (and (symbolp mac)
                             (plist-worldp wrld))))
 (let
  ((__function__ 'macro-args+))
  (declare (ignorable __function__))
  (if
   (not (macro-symbolp mac wrld))
   (raise "The symbol ~x0 does not name a macro."
          mac)
   (b*
    ((result (macro-args mac wrld)))
    (if
     (true-listp result)
     result
     (raise
      "Internal error: ~
                the MACRO-ARGS property ~x0 of ~x1 is not a true list."
      result mac))))))

Theorem: true-listp-of-macro-args+

(defthm true-listp-of-macro-args+
        (b* ((result (macro-args+ mac wrld)))
            (true-listp result))
        :rule-classes :rewrite)