		Search-engine friendly clone of the ACL2 documentation.

Casesplit-input-processing

Casesplit-process-conditions

Process the conditions input.

Signature
(casesplit-process-conditions conditions old$ verify-guards$ ctx state) → (mv erp conditions$ state)
Arguments: old$ — Guard (symbolp old$).; verify-guards$ — Guard (booleanp verify-guards$).
Returns: conditions$ — A pseudo-term-listp.

Definitions and Theorems

Function: casesplit-process-conditions-aux

(defun casesplit-process-conditions-aux
       (conditions 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-conditions-aux))
    (declare (ignorable __function__))
    (cond ((endp conditions) (value nil))
          (t (b* (((er cond$)
                   (casesplit-process-condition
                        (car conditions)
                        pos old$ verify-guards$ ctx state))
                  ((er conditions$)
                   (casesplit-process-conditions-aux
                        (cdr conditions)
                        (1+ pos)
                        old$ verify-guards$ ctx state)))
               (value (cons cond$ conditions$)))))))

Function: casesplit-process-conditions

(defun casesplit-process-conditions
       (conditions old$ verify-guards$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old$)
                             (booleanp verify-guards$))))
 (let ((__function__ 'casesplit-process-conditions))
  (declare (ignorable __function__))
  (b*
   (((unless (true-listp conditions))
     (er-soft+
      ctx t nil
      "The second input must be a true list, ~
                   but it is ~x0 instead."
      conditions))
    ((unless (consp conditions))
     (er-soft+
      ctx t nil
      "The second input must be a non-empty list, ~
                   but it is ~x0 instead."
      conditions))
    (pos 1))
   (casesplit-process-conditions-aux
        conditions
        pos old$ verify-guards$ ctx state))))