		Search-engine friendly clone of the ACL2 documentation.

Input-processors

Process-input-new-enable

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

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

The APT transformations that use this utility have a :new-enable input that specifies whether to enable or not the new function. This input must be a boolean or :auto (the default). If it is :auto, the new function is enabled iff the old one is. In any case, this utility returns a boolean saying whether the new function is enabled or not.

Definitions and Theorems

Function: process-input-new-enable

(defun process-input-new-enable (new-enable old ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (symbolp old)))
 (let ((__function__ 'process-input-new-enable))
  (declare (ignorable __function__))
  (cond
   ((eq new-enable t) (value t))
   ((eq new-enable nil) (value nil))
   ((eq new-enable :auto)
    (value (fundef-enabledp old state)))
   (t
    (er-soft+
     ctx t nil
     "The :NEW-ENABLE input must be T, NIL, or :AUTO, ~
                      but it is ~x0 instead."
     new-enable)))))

Theorem: booleanp-of-process-input-new-enable.enable

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