Process the
(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)
The APT transformations that use this utility
have an
The caller of this utility must set
the parameter
Function:
(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:
(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)