Included Books
other
(in-package "ACL2")
other
(program)
other
(set-state-ok t)
include-book
(include-book "elide-event")
get-event-local-pfunction
(defun get-event-local-p (n wrld) (let ((event-tuple (cddr (car (lookup-world-index 'event n wrld))))) (and event-tuple (access-event-tuple-local-p event-tuple))))
fns-with-abs-ev-between-or-localfunction
(defun fns-with-abs-ev-between-or-local (names min max wrld acc) (cond ((endp names) acc) (t (fns-with-abs-ev-between-or-local (cdr names) min max wrld (let ((k (getpropc (car names) 'absolute-event-number 0 wrld))) (cond ((or (and (< min k) (<= k max)) (get-event-local-p k wrld)) (cons (car names) acc)) (t acc)))))))
instantiable-ancestors-with-guards/measuresfunction
(defun instantiable-ancestors-with-guards/measures (fns wrld ans seen) (cond ((null fns) (mv ans seen)) ((hons-get (car fns) seen) (instantiable-ancestors-with-guards/measures (cdr fns) wrld ans seen)) (t (let* ((ans1 (cons (car fns) ans)) (seen (hons-acons (car fns) t seen)) (imm (immediate-instantiable-ancestors (car fns) wrld ans1)) (guard (getpropc (car fns) 'guard nil wrld)) (just (getpropc (car fns) 'justification nil wrld)) (measure (and just (access justification just :measure))) (imm1 (if guard (all-fnnames1 nil guard imm) imm)) (imm2 (if (and (consp measure) (not (eq (car measure) :?))) (all-fnnames1 nil measure imm1) imm1))) (mv-let (ans2 seen) (instantiable-ancestors-with-guards/measures imm2 wrld ans1 seen) (instantiable-ancestors-with-guards/measures (cdr fns) wrld ans2 seen))))))
accumulate-macro-names-from-aliasesfunction
(defun accumulate-macro-names-from-aliases (names macro-aliases acc) (cond ((endp names) acc) (t (accumulate-macro-names-from-aliases (cdr names) macro-aliases (let ((pair (rassoc (car names) macro-aliases))) (cond (pair (cons (car pair) acc)) (t acc)))))))
get-event+function
(defun get-event+ (name fal wrld) (let ((index (getpropc name 'absolute-event-number nil wrld))) (cond ((null index) (mv :failed nil)) ((hons-get index fal) (mv nil nil)) (t (let ((ev (access-event-tuple-form (cddr (car (lookup-world-index 'event index wrld)))))) (mv index (if (eq (car ev) 'defconst) (assert$ (eq (cadr ev) name) `(defconst ,NAME ,(GETPROPC NAME 'CONST NIL WRLD))) ev)))))))
constant-name-pfunction
(defun constant-name-p (form) (and (symbolp form) (let* ((s (symbol-name form)) (len (length s))) (and (not (= len 0)) (eql (char s 0) #\*) (eql (char s (1- len)) #\*)))))
supporters-macro-formsfunction
(defun supporters-macro-forms (form) (declare (xargs :guard (true-listp form))) (cond ((eq (car form) 'mbe) (mv t (list (cadr (assoc-keyword :logic (cdr form))) (cadr (assoc-keyword :exec (cdr form)))))) ((member-eq (car form) '(value or and first rest second third fourth caar cdar cadr cddr caddr cdddr ffn-symb fargs fargn assoc assoc-eq prog2$ progn$ pprogn er-progn list list* append <= > >= + * / - logior logand lognot logxor acl2-unwind-protect cw member-eq union-eq set-difference-eq union$ set-difference$ fms-to-string fms!-to-string fmt-to-string fmt!-to-string fmt1-to-string fmt1!-to-string getprop getpropc set-inhibit-output-lst f-get-global f-boundp-global revert-world)) (mv t (cdr form))) ((member-eq (car form) '(check-vars-not-free concatenate f-put-global mv-let warn-about-parallelism-hazard)) (mv t (cddr form))) ((eq (car form) '@) (mv t nil)) ((eq (car form) 'cond) (mv t (append-lst (cdr form)))) ((eq (car form) 'case) (mv t (cons (cadr form) (strip-cadrs (cddr form))))) (t (mv nil nil))))
collect-constants-and-macros-1mutual-recursion
(mutual-recursion (defun collect-constants-and-macros-1 (form acc wrld state-vars) (cond ((booleanp form) acc) ((constant-name-p form) (cons form acc)) ((not (true-listp form)) acc) ((member-eq (car form) ''lambda$) acc) ((member-eq (car form) '(let let* er-let*)) (let ((bindings (cadr form))) (collect-constants-and-macros-lst (and (doublet-listp bindings) (strip-cadrs bindings)) (collect-constants-and-macros-1 (car (last form)) acc wrld state-vars) wrld state-vars))) ((eq (car form) 'stobj-let) (collect-constants-and-macros-lst (cdddr form) acc wrld state-vars)) ((and (consp (car form)) (eq (caar form) 'lambda) (true-listp (car form))) (collect-constants-and-macros-1 (car (last (car form))) (collect-constants-and-macros-lst (cdr form) acc wrld state-vars) wrld state-vars)) (t (mv-let (flg lst) (supporters-macro-forms form) (cond (flg (collect-constants-and-macros-lst lst acc wrld state-vars)) ((getpropc (car form) 'macro-body nil wrld) (mv-let (erp expansion) (macroexpand1-cmp form 'some-ctx wrld state-vars) (cond (erp acc) (t (collect-constants-and-macros-1 expansion (cons (car form) acc) wrld state-vars))))) (t (collect-constants-and-macros-lst (cdr form) acc wrld state-vars))))))) (defun collect-constants-and-macros-lst (lst acc wrld state-vars) (cond ((endp lst) acc) (t (collect-constants-and-macros-1 (car lst) (collect-constants-and-macros-lst (cdr lst) acc wrld state-vars) wrld state-vars)))))
guard-from-eventfunction
(defun guard-from-event (ev wrld) (mv-let (dcls guard) (dcls-guard-raw-from-def (cdr ev) wrld) (declare (ignore dcls)) guard))
collect-constants-and-macros-evmutual-recursion
(mutual-recursion (defun collect-constants-and-macros-ev (ev acc wrld state-vars) (assert$ (true-listp ev) (case (car ev) ((defun defund defun-nx defund-nx defmacro) (let* ((guard (guard-from-event ev wrld)) (acc (if guard (collect-constants-and-macros-1 guard acc wrld state-vars) acc))) (collect-constants-and-macros-1 (car (last ev)) acc wrld state-vars))) (defchoose (collect-constants-and-macros-1 (car (last ev)) acc wrld state-vars)) (mutual-recursion (collect-constants-and-macros-ev-lst (cdr ev) acc wrld state-vars)) ((defthm defaxiom defconst deftheory) (collect-constants-and-macros-1 (caddr ev) acc wrld state-vars)) (defchoose (collect-constants-and-macros-1 (nth 4 ev) acc wrld state-vars)) (table (collect-constants-and-macros-lst (cddr ev) acc wrld state-vars)) (otherwise acc)))) (defun collect-constants-and-macros-ev-lst (ev-lst acc wrld state-vars) (cond ((endp ev-lst) acc) (t (collect-constants-and-macros-ev (car ev-lst) (collect-constants-and-macros-ev-lst (cdr ev-lst) acc wrld state-vars) wrld state-vars)))))
supporters-extend-seenfunction
(defun supporters-extend-seen (fns seen) (cond ((endp fns) seen) (t (supporters-extend-seen (cdr fns) (hons-acons (car fns) t seen)))))
filter-out-seenfunction
(defun filter-out-seen (lst seen) (cond ((endp lst) nil) ((hons-get (car lst) seen) (filter-out-seen (cdr lst) seen)) (t (cons (car lst) (filter-out-seen (cdr lst) seen)))))
absstobj-supportersfunction
(defun absstobj-supporters (absstobj-tuples) (cond ((endp absstobj-tuples) nil) (t (let ((tuple (car absstobj-tuples))) (list* (cadr tuple) (caddr tuple) (if (cdddr tuple) (cons (cdddr tuple) (absstobj-supporters (cdr absstobj-tuples))) (absstobj-supporters (cdr absstobj-tuples))))))))
supporters-of-1-lstmutual-recursion
(mutual-recursion (defun supporters-of-1-lst (defs min max macro-aliases wrld state-vars seen) (cond ((endp defs) (mv nil seen)) (t (mv-let (lst1 seen) (supporters-of-1 (car defs) min max macro-aliases wrld state-vars seen) (mv-let (lst2 seen) (supporters-of-1-lst (cdr defs) min max macro-aliases wrld state-vars seen) (mv (append lst1 lst2) seen)))))) (defun supporters-of-1 (ev min max macro-aliases wrld state-vars seen) (cond ((and (consp ev) (eq (car ev) 'mutual-recursion)) (supporters-of-1-lst (cdr ev) min max macro-aliases wrld state-vars seen)) (t (let* ((non-trivial-encapsulate-p (and (consp ev) (eq (car ev) 'encapsulate) (cadr ev))) (name (if non-trivial-encapsulate-p (let ((sig (car (cadr ev)))) (if (symbolp (car sig)) (car sig) (caar sig))) (and (consp ev) (consp (cdr ev)) (symbolp (cadr ev)) (cadr ev))))) (cond ((null name) (mv nil seen)) (t (let* ((formula (if non-trivial-encapsulate-p (mv-let (name2 x origins) (constraint-info name wrld) (declare (ignore origins)) (cond ((unknown-constraints-p x) *t*) (name2 (conjoin x)) (t x))) (or (getpropc name 'macro-body nil wrld) (formula name nil wrld)))) (guard (getpropc name 'guard nil wrld)) (attachment-prop (attachment-alist name wrld)) (attachment-alist (and (not (eq (car attachment-prop) :attachment-disallowed)) attachment-prop)) (absstobj-info (and (consp ev) (eq (car ev) 'defabsstobj) (getpropc (cadr ev) 'absstobj-info nil wrld))) (absstobj-supporters (and absstobj-info (absstobj-supporters (cdr absstobj-info)))) (new-fns (and (or formula absstobj-supporters attachment-alist) (all-fnnames1 nil formula (and (or absstobj-supporters guard attachment-alist) (all-fnnames1 nil guard (append absstobj-supporters (strip-cars attachment-alist) (strip-cdrs attachment-alist))))))) (new-fns (filter-out-seen new-fns seen))) (mv-let (new-fns seen) (instantiable-ancestors-with-guards/measures (fns-with-abs-ev-between-or-local new-fns min max wrld nil) wrld nil seen) (let* ((new-fns (fns-with-abs-ev-between-or-local new-fns min max wrld nil)) (new-names (if non-trivial-encapsulate-p (collect-constants-and-macros-1 formula new-fns wrld state-vars) (collect-constants-and-macros-ev ev new-fns wrld state-vars)))) (mv (accumulate-macro-names-from-aliases new-fns macro-aliases new-names) seen)))))))))))
supporters-of-recfunction
(defun supporters-of-rec (lst fal min max macro-aliases ctx wrld state-vars seen) (cond ((endp lst) (mv fal seen)) (t (let ((constraint-lst (and (symbolp (car lst)) (pre-v8-7-getpropc-constraint-lst-nil (car lst) wrld)))) (cond ((and constraint-lst (symbolp constraint-lst)) (supporters-of-rec (cons constraint-lst (cdr lst)) fal min max macro-aliases ctx wrld state-vars seen)) (t (mv-let (n ev) (cond ((symbolp (car lst)) (get-event+ (car lst) fal wrld)) ((hons-get (caar lst) fal) (mv nil nil)) (t (mv (caar lst) (cdar lst)))) (cond ((null n) (supporters-of-rec (cdr lst) fal min max macro-aliases ctx wrld state-vars seen)) ((eq n :failed) (mv (er hard ctx "The name ~x0 is not defined, yet it was expected to be." (car lst)) nil)) (t (mv-let (fns seen) (supporters-of-1 ev min max macro-aliases wrld state-vars seen) (supporters-of-rec (append fns (cdr lst)) (hons-acons n ev fal) min max macro-aliases ctx wrld state-vars seen)))))))))))
adjust-defun-for-symbol-classfunction
(defun adjust-defun-for-symbol-class (ev wrld) (flet ((add-dcl-to-defun (dcl ev) `(,(CAR EV) ,(CADR EV) ,(CADDR EV) (declare ,DCL) ,@(CDDDR EV)))) (case (symbol-class (cadr ev) wrld) (:program (add-dcl-to-defun '(xargs :mode :program) ev)) (:ideal (add-dcl-to-defun '(xargs :mode :logic :verify-guards nil) ev)) (otherwise `(progn ,EV (verify-guards ,(CADR EV)))))))
adjust-encapsulate-for-symbol-classfunction
(defun adjust-encapsulate-for-symbol-class (ev wrld) (let ((name (case-match ev (('encapsulate (((name . &) . &) . &) . &) name) (('encapsulate ((name . &) . &) . &) name) (& nil)))) (cond (name (let* ((wrld-tail (lookup-world-index 'event (getpropc name 'absolute-event-number 0 wrld) wrld)) (old-vge (default-verify-guards-eagerness wrld-tail)) (new-vge (default-verify-guards-eagerness wrld))) (cond ((eql old-vge new-vge) ev) (t `(encapsulate nil (set-verify-guards-eagerness ,OLD-VGE) ,EV))))) (t ev))))
adjust-ev-for-symbol-classfunction
(defun adjust-ev-for-symbol-class (ev wrld) (case (car ev) (defchoose `(encapsulate nil (logic) ,EV)) ((defun defund defun-nx defund-nx) (adjust-defun-for-symbol-class ev wrld)) (mutual-recursion (let ((def1 (adjust-defun-for-symbol-class (cadr ev) wrld))) (if (eq (car def1) 'progn) `(progn ,EV ,(CADDR DEF1)) `(mutual-recursion ,DEF1 ,@(CDDR EV))))) (encapsulate (adjust-encapsulate-for-symbol-class ev wrld)) (otherwise ev)))
events-from-supporters-falfunction
(defun events-from-supporters-fal (pairs min max wrld acc) (cond ((or (endp pairs) (< max (caar pairs))) (reverse acc)) ((and (<= (car (car pairs)) min) (not (get-event-local-p (car (car pairs)) wrld))) (events-from-supporters-fal (cdr pairs) min max wrld acc)) (t (events-from-supporters-fal (cdr pairs) min max wrld (cons (adjust-ev-for-symbol-class (cdr (car pairs)) wrld) acc)))))
get-defattach-event-fnfunction
(defun get-defattach-event-fn (ev) (case-match ev (('defattach (f . &) . &) f) (('defattach f &) f) (& nil)))
defattach-event-lstfunction
(defun defattach-event-lst (wrld fns min max acc seen) (let ((trip (car wrld))) (cond ((and (eq (car trip) 'event-landmark) (eq (cadr trip) 'global-value)) (cond ((<= (access-event-tuple-number (cddr trip)) min) acc) ((or (> (access-event-tuple-number (cddr trip)) max) (not (eq (car (access-event-tuple-form (cddr trip))) 'defattach))) (defattach-event-lst (cdr wrld) fns min max acc seen)) (t (let* ((ev (access-event-tuple-form (cddr trip))) (fn (get-defattach-event-fn ev))) (cond ((and fn (not (member-eq fn seen)) (member-eq fn fns)) (defattach-event-lst (cdr wrld) fns min max (cons ev acc) (cons fn seen))) (t (defattach-event-lst (cdr wrld) fns min max acc seen))))))) (t (defattach-event-lst (cdr wrld) fns min max acc seen)))))
supporter-fns-in-range-or-localfunction
(defun supporter-fns-in-range-or-local (alist min max wrld acc) (cond ((endp alist) acc) (t (supporter-fns-in-range-or-local (cdr alist) min max wrld (if (or (not (function-symbolp (caar alist) wrld)) (let ((n (getpropc (caar alist) 'absolute-event-number nil wrld))) (and (or (<= n min) (< max n)) (not (get-event-local-p n wrld))))) acc (cons (caar alist) acc))))))
supporters-offunction
(defun supporters-of (lst min max ctx wrld state-vars) (mv-let (fal seen) (supporters-of-rec lst nil min max (macro-aliases wrld) ctx wrld state-vars nil) (let* ((x (merge-sort-car-< (fast-alist-free fal))) (fns (supporter-fns-in-range-or-local (fast-alist-free seen) min max wrld nil))) (cons (append? (events-from-supporters-fal x min max wrld nil) (defattach-event-lst wrld fns min max nil nil)) fns))))
table-info-after-kfunction
(defun table-info-after-k (names wrld k evs table-guard-fns) (let ((trip (car wrld))) (cond ((and (eq (car trip) 'event-landmark) (eq (cadr trip) 'global-value)) (cond ((<= (access-event-tuple-number (cddr trip)) k) (mv evs table-guard-fns)) (t (let* ((ev (access-event-tuple-form (cddr trip))) (evs (case-match ev (('table name nil nil :guard &) (cond ((eq name 'pe-table) evs) ((or (eq names :all) (member-eq name names)) (cons ev evs)) (t evs))) (('table name . &) (cond ((eq name 'pe-table) evs) ((and (not (member-eq name '(acl2-defaults-table xdoc))) (or (eq names :all) (member-eq name names)) (not (assoc-eq-cadr name evs))) (cons `(table ,NAME nil ',(TABLE-ALIST NAME WRLD) :clear) evs)) (t evs))) (& evs)))) (table-info-after-k names (cdr wrld) k evs table-guard-fns))))) ((and (eq (cadr trip) 'table-guard) (not (eq (cddr trip) *acl2-property-unbound*))) (table-info-after-k names (cdr wrld) k evs (all-fnnames1 nil (cddr trip) table-guard-fns))) (t (table-info-after-k names (cdr wrld) k evs table-guard-fns)))))
supporters-in-theory-eventfunction
(defun supporters-in-theory-event (fns ens wrld min disables) (cond ((endp fns) (and disables `(in-theory (disable ,@DISABLES)))) (t (supporters-in-theory-event (cdr fns) ens wrld min (if (and min (<= (getpropc (car fns) 'absolute-event-number nil wrld) min)) disables (append (disabledp-fn (car fns) ens wrld) disables))))))
wsa-ermacro
(defmacro wsa-er (str &rest args) `(mv (er hard 'with-supporters ,STR ,@ARGS) nil nil nil nil))
*with-supporters-with-output-default*constant
(defconst *with-supporters-with-output-default* '(:off :all :on (error)))
with-supporters-argsfunction
(defun with-supporters-args (events names tables show with-output with-output-p) (cond ((null events) (mv names tables show (if with-output-p with-output '(:off :all :on error)) nil)) ((eq (car events) :names) (cond ((null (cdr events)) (wsa-er "No argument was supplied for :NAMES.")) ((not (symbol-listp (cadr events))) (wsa-er "The value of :NAMES must be a list of symbols, which ~ ~x0 is not." (cadr events))) (t (with-supporters-args (cddr events) (cadr events) tables show with-output with-output-p)))) ((eq (car events) :tables) (cond ((null (cdr events)) (wsa-er "No argument was supplied for :TABLES.")) ((not (or (eq (cadr events) :all) (symbol-listp (cadr events)))) (wsa-er "The value of :TABLES must be :ALL or a list of ~ symbols, but ~x0 is neither." (cadr events))) (t (with-supporters-args (cddr events) names (cadr events) show with-output with-output-p)))) ((eq (car events) :show) (cond ((null (cdr events)) (wsa-er "No argument was supplied for :SHOW.")) ((not (member-eq (cadr events) '(t nil :only))) (wsa-er "The value of :SHOW must be Boolean or :ONLY, but ~ ~x0 is not." (cadr events))) (t (with-supporters-args (cddr events) names tables (cadr events) with-output with-output-p)))) ((eq (car events) :with-output) (cond ((null (cdr events)) (wsa-er "No argument was supplied for :WITH-OUTPUT.")) ((not (keyword-value-listp (cadr events))) (wsa-er "The value of :WITH-OUTPUT must satisfy ~x0, but ~x1 ~ does not." 'keyword-value-listp (cadr events))) (t (with-supporters-args (cddr events) names tables show (cadr events) t)))) ((atom (car events)) (wsa-er "An event must be a cons, but your first event was ~x0. ~ Perhaps you intended to use :NAMES." (car events))) ((or (member-eq :names events) (member-eq :tables events) (member-eq :show events) (member-eq :with-output events)) (wsa-er "The :NAMES, and :TABLES keywords of WITH-SUPPORTERS must ~ appear immediately after the (initial) LOCAL event.")) (t (mv names tables show (if with-output-p with-output '(:off :all :on error)) events))))
event-pairs-afterfunction
(defun event-pairs-after (k wrld acc) (let ((trip (car wrld))) (cond ((and (eq (car trip) 'event-landmark) (eq (cadr trip) 'global-value)) (let ((n (access-event-tuple-number (cddr trip)))) (cond ((<= n k) acc) (t (event-pairs-after k (cdr wrld) (cons (cons n (access-event-tuple-form (cddr trip))) acc)))))) (t (event-pairs-after k (cdr wrld) acc)))))
with-supporters-fnfunction
(defun with-supporters-fn (local-event rest) (cond ((not (and (true-listp local-event) (eq (car local-event) 'local) (consp (cdr local-event)) (null (cddr local-event)))) (er hard 'with-supporters "The first argument of ~x0 should be of the form (LOCAL ...), but ~ that argument is ~x1." 'with-supporters local-event)) ((member-eq :names (cdr (member-eq :names rest))) (er hard 'with-supporters "A :NAMES argument may not occur more than once in a call of ~x0." 'with-supporters)) (t (mv-let (names tables show with-output events) (with-supporters-args rest nil nil nil nil nil) (let* ((form `(let ((min (cdr (assoc-eq :min (table-alist 'with-supporters-table (w state))))) (ctx 'with-supporters)) (er-progn ,(CADR LOCAL-EVENT) (let* ((wrld (w state)) (max (max-absolute-event-number wrld))) (mv-let (table-evs fns1) (table-info-after-k ',TABLES wrld min nil nil) (er-progn (progn ,@EVENTS) (let* ((wrld (w state)) (event-pairs (event-pairs-after max wrld nil)) (extras/fns (supporters-of (append fns1 ',NAMES event-pairs) min max ctx wrld (default-state-vars t))) (extras (car extras/fns)) (fns (cdr extras/fns)) (in-theory-event (supporters-in-theory-event fns (ens state) wrld min nil)) (ev (list* 'progn ',LOCAL-EVENT '(set-enforce-redundancy t) '(set-bogus-defun-hints-ok t) '(set-bogus-mutual-recursion-ok t) '(set-irrelevant-formals-ok t) '(set-ignore-ok t) '(set-state-ok t) (append (elide-event-lst extras) table-evs (and in-theory-event (list in-theory-event)) (cons '(set-enforce-redundancy nil) ',EVENTS)))) ,@(AND WITH-OUTPUT `((EV (CONS 'WITH-OUTPUT (APPEND ',WITH-OUTPUT (LIST EV))))))) ,(CASE SHOW (:ONLY '(VALUE (LIST 'VALUE-TRIPLE (LIST 'QUOTE EV)))) ((T) '(PPROGN (FMS "Expansion of with-supporters call:~|~x0~|" (LIST (CONS #\0 EV)) (STANDARD-CO STATE) STATE NIL) (VALUE EV))) ((NIL) '(VALUE EV)) (OTHERWISE (ER HARD 'WITH-SUPPORTERS "Illegal value of :show, ~x0" SHOW))))))))))) (if with-output `(with-output ,@WITH-OUTPUT (encapsulate nil (local (table with-supporters-table :min (max-absolute-event-number world))) ,LOCAL-EVENT (make-event ,FORM))) `(encapsulate nil (local (table with-supporters-table :min (max-absolute-event-number world))) ,LOCAL-EVENT (make-event ,FORM))))))))
with-supportersmacro
(defmacro with-supporters (local-event &rest rest) (with-supporters-fn local-event rest))
with-supporters-after-fnfunction
(defun with-supporters-after-fn (name events) `(make-event (let ((min (getprop ',NAME 'absolute-event-number nil 'current-acl2-world (w state))) (max (max-absolute-event-number (w state)))) (cond ((null min) (er soft 'with-supporters "The symbol ~x0 does not seem to be the name of an event." ',NAME)) (t (er-progn (progn ,@EVENTS) (let* ((wrld (w state)) (event-pairs (event-pairs-after max wrld nil)) (extras/fns (supporters-of event-pairs min max 'with-supporters-after wrld (default-state-vars t))) (extras (car extras/fns)) (fns (cdr extras/fns)) (in-theory-event (supporters-in-theory-event fns (ens state) (w state) nil nil))) (value (list* 'progn '(set-enforce-redundancy t) '(set-bogus-defun-hints-ok t) '(set-bogus-mutual-recursion-ok t) '(set-irrelevant-formals-ok t) '(set-ignore-ok t) (append extras (and in-theory-event (list in-theory-event)) (cons '(set-enforce-redundancy nil) ',EVENTS)))))))))))
with-supporters-aftermacro
(defmacro with-supporters-after (name &rest events) (declare (xargs :guard (symbolp name))) (with-supporters-after-fn name events))