		Search-engine friendly clone of the ACL2 documentation.

Casesplit-input-processing

Casesplit-process-condition

Process an element of the conditions input.

Signature
(casesplit-process-condition cond pos old$ verify-guards$ ctx state) → (mv erp condition$ state)
Arguments: cond — An element of conditions.; pos — Position of cond in conditions, 1-based.
Guard (posp pos).; old$ — Guard (symbolp old$).; verify-guards$ — Guard (booleanp verify-guards$).
Returns: condition$ — A pseudo-termp that is the translation of cond.

Definitions and Theorems

Function: casesplit-process-condition

(defun casesplit-process-condition
       (cond pos old$ verify-guards$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (posp pos)
                             (symbolp old$)
                             (booleanp verify-guards$))))
 (let ((__function__ 'casesplit-process-condition))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    (description (msg "The ~n0 element of the second input"
                      (list pos)))
    ((er (list term stobjs-out))
     (ensure-value-is-untranslated-term$ cond description t nil))
    (description (msg "The term ~x0 that denotes the ~n1 condition"
                      cond (list pos)))
    ((er &)
     (ensure-term-free-vars-subset$ term (formals old$ wrld)
                                    description t nil))
    ((er &)
     (ensure-term-logic-mode$ term description t nil))
    ((er &)
     (ensure-function/lambda/term-number-of-results$
          stobjs-out 1 description t nil))
    ((er &)
     (ensure-term-no-stobjs$ stobjs-out description t nil))
    ((er &)
     (if verify-guards$
      (ensure-term-guard-verified-exec-fns$
       term
       (msg
        "Since either the :VERIFY-GUARDS input is T, ~
                          or it is (perhaps by default) :AUTO ~
                          and the target function ~x0 is guard-verified, ~@1"
        old$ (msg-downcase-first description))
       t nil)
      (value nil)))
    ((er &)
     (ensure-term-does-not-call$ term old$ description t nil)))
   (value term))))