Enhanced variant of macro-args.
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
(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))))))
(defthm true-listp-of-macro-args+ (b* ((result (macro-args+ mac wrld))) (true-listp result)) :rule-classes :rewrite)