		Search-engine friendly clone of the ACL2 documentation.

Parteval-input-processing

Parteval-process-old

Process the old input.

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

Definitions and Theorems

Function: parteval-process-old

(defun parteval-process-old (old verify-guards ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'parteval-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-is-defined$ 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 :this-is-irrelevant))))
   (value old$))))

Theorem: symbolp-of-parteval-process-old.old$

(defthm symbolp-of-parteval-process-old.old$
  (b* (((mv ?erp ?old$ acl2::?state)
        (parteval-process-old old verify-guards ctx state)))
    (symbolp old$))
  :rule-classes :rewrite)