		Search-engine friendly clone of the ACL2 documentation.

Input-processors

Process-input-old-to-new-enable

Process the :old-to-new-enable input of an APT transformation.

Signature
(process-input-old-to-new-enable old-to-new-enable old-to-new-enable-present ctx state) → (mv erp processed-old-to-new-enable state)
Arguments: old-to-new-enable-present — Guard (booleanp old-to-new-enable-present).
Returns: processed-old-to-new-enable — Type (booleanp processed-old-to-new-enable).

The APT transformations that use this utility have an :old-to-new-enable input that specifies whether to enable or not the theorem that rewrites the old function in terms of the new function. This must be a boolean. If absent, it is taken from the APT defaults table; see set-default-input-old-to-new-enable.

The caller of this utility must set the parameter old-to-new-enable-present to t iff the :old-to-new-enable input is present. If this is nil, the parameter old-to-new-enable is ignored.

Definitions and Theorems

Function: process-input-old-to-new-enable

(defun process-input-old-to-new-enable
       (old-to-new-enable old-to-new-enable-present ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (booleanp old-to-new-enable-present)))
  (let ((__function__ 'process-input-old-to-new-enable))
    (declare (ignorable __function__))
    (if old-to-new-enable-present
        (b* (((er &)
              (ensure-value-is-boolean$
                   old-to-new-enable
                   "The :OLD-TO-NEW-ENABLE input" t nil)))
          (value old-to-new-enable))
      (value (get-default-input-old-to-new-enable (w state))))))

Theorem: booleanp-of-process-input-old-to-new-enable.processed-old-to-new-enable

(defthm
 booleanp-of-process-input-old-to-new-enable.processed-old-to-new-enable
 (b* (((mv ?erp ?processed-old-to-new-enable
           acl2::?state)
       (process-input-old-to-new-enable
            old-to-new-enable
            old-to-new-enable-present ctx state)))
   (booleanp processed-old-to-new-enable))
 :rule-classes :rewrite)