Set the default
Some APT transformations include an
This macro sets an entry in the APT defaults table
that provides the default value of the
The initial value of this default is
Macro:
(defmacro set-default-input-old-to-new-enable (bool) (declare (xargs :guard (booleanp bool))) (b* ((ctx (cons 'set-default-input-old-to-new-enable bool))) (cons 'make-event-terse (cons (cons 'set-default-input-old-to-new-enable-fn (cons bool (cons (cons 'quote (cons ctx 'nil)) '(state)))) 'nil))))
Function:
(defun set-default-input-old-to-new-enable-fn (bool ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (booleanp bool))) (let ((__function__ 'set-default-input-old-to-new-enable-fn)) (declare (ignorable __function__)) (b* ((table (table-alist+ *defaults-table-name* (w state)) ) (pair (assoc-eq :new-to-old-enable table))) (if (and (consp pair) (cdr pair) bool) (er-soft+ ctx t nil "Since the :NEW-TO-OLD-ENABLE default is T, ~ the :OLD-TO-NEW-ENABLE default cannot be set to T. ~ At most one of these two defaults may be T at any time.") (value (cons 'table (cons *defaults-table-name* (cons ':old-to-new-enable (cons bool 'nil)))))))))