		Search-engine friendly clone of the ACL2 documentation.

Input-processors

Process-input-new-to-old-enable

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

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

This is quite analogous to process-input-old-to-new-enable, but for the :new-to-old-enable input of an APT transformation.

Definitions and Theorems

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

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

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

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