		Search-engine friendly clone of the ACL2 documentation.

Defaults-table

Set-default-input-new-to-old-enable

Set the default :new-to-old-enable input of APT transformations.

Some APT transformations include a :new-to-old-enable input that specifies whether to enable the generated theorem that rewrites (a term involving) a call of the old function to (a term involving) a call of the new function.

This macro sets an entry in the APT defaults table that provides the default value of the :new-to-old-enable input. It must be a boolean. It cannot be t if the default :old-to-new-enable is currently t.

The initial value of this default is nil.

Macro: set-default-input-new-to-old-enable

(defmacro set-default-input-new-to-old-enable (bool)
  (declare (xargs :guard (booleanp bool)))
  (b* ((ctx (cons 'set-default-input-new-to-old-enable
                  bool)))
    (cons 'make-event-terse
          (cons (cons 'set-default-input-new-to-old-enable-fn
                      (cons bool
                            (cons (cons 'quote (cons ctx 'nil))
                                  '(state))))
                'nil))))

Definitions and Theorems

Function: set-default-input-new-to-old-enable-fn

(defun set-default-input-new-to-old-enable-fn (bool ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (booleanp bool)))
 (let ((__function__ 'set-default-input-new-to-old-enable-fn))
  (declare (ignorable __function__))
  (b* ((table (table-alist+ *defaults-table-name* (w state))
)
       (pair (assoc-eq :old-to-new-enable table)))
   (if
    (and (consp pair) (cdr pair) bool)
    (er-soft+
     ctx t nil
     "Since the :OLD-TO-NEW-ENABLE default is T, ~
                     the :NEW-TO-OLD-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 ':new-to-old-enable
                             (cons bool 'nil)))))))))