Process the
(process-input-old-to-wrapper-enable old-to-wrapper-enable old-to-wrapper-enable-present gen-wrapper ctx state) → (mv erp processed-old-to-wrapper-enable state)
This is quite analogous to process-input-old-to-new-enable,
but for the
Function:
(defun process-input-old-to-wrapper-enable (old-to-wrapper-enable old-to-wrapper-enable-present gen-wrapper ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (booleanp old-to-wrapper-enable-present) (booleanp gen-wrapper)))) (let ((__function__ 'process-input-old-to-wrapper-enable)) (declare (ignorable __function__)) (if gen-wrapper (if old-to-wrapper-enable-present (b* (((er &) (ensure-value-is-boolean$ old-to-wrapper-enable "The :OLD-TO-WRAPPER-ENABLE input" t nil))) (value old-to-wrapper-enable)) (value (get-default-input-old-to-wrapper-enable (w state)))) (if old-to-wrapper-enable-present (er-soft+ ctx t nil "Since the :WRAPPER input is (perhaps by default) NIL, ~ no :OLD-TO-WRAPPER-ENABLE input may be supplied, but ~x0 was supplied instead." old-to-wrapper-enable) (value nil)))))
Theorem:
(defthm booleanp-of-process-input-old-to-wrapper-enable.processed-old-to-wrapper-enable (b* (((mv ?erp ?processed-old-to-wrapper-enable acl2::?state) (process-input-old-to-wrapper-enable old-to-wrapper-enable old-to-wrapper-enable-present gen-wrapper ctx state))) (booleanp processed-old-to-wrapper-enable)) :rule-classes :rewrite)