		Search-engine friendly clone of the ACL2 documentation.

Casesplit-input-processing

Casesplit-process-old

Process the old input.

Signature
(casesplit-process-old old verify-guards ctx state) → (mv erp old$ state)
Returns: old$ — A symbolp that is the name of the target function of the transformation, denoted by the old input.

Definitions and Theorems

Function: casesplit-process-old

(defun casesplit-process-old (old verify-guards ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'casesplit-process-old))
  (declare (ignorable __function__))
  (b*
   (((er old$)
     (ensure-function-name-or-numbered-wildcard$
          old "The first input" t nil))
    (description (msg "The target function ~x0" old$))
    ((er &)
     (ensure-function-is-logic-mode$ old$ description t nil))
    ((er &)
     (ensure-function-number-of-results$ old$ 1 description t nil))
    ((er &)
     (ensure-function-no-stobjs$ old$ description t nil))
    ((er &)
     (if
      (eq verify-guards t)
      (ensure-function-is-guard-verified$
       old$
       (msg
        "Since the :VERIFY-GUARDS input is T, ~
                          the target function ~x0"
        old$)
       t nil)
      (value nil))))
   (value old$))))