		Search-engine friendly clone of the ACL2 documentation.

Casesplit-input-processing

Casesplit-process-theorems

Process the theorems input.

Signature
(casesplit-process-theorems theorems old$ conditions$ ctx state) → (mv erp hyps-news state)
Arguments: old$ — Guard (symbolp old$).; conditions$ — Guard (pseudo-term-listp conditions$).
Returns: hyps-news — A tuple (hyps news) satisfying (typed-tuple pseudo-term-listp pseudo-term-listp hyps-news).

Definitions and Theorems

Function: casesplit-process-theorems-aux

(defun casesplit-process-theorems-aux (theorems pos old$ ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (posp pos) (symbolp old$))))
  (let ((__function__ 'casesplit-process-theorems-aux))
    (declare (ignorable __function__))
    (cond ((endp theorems) (value (list nil nil)))
          (t (b* (((er (list hyp new))
                   (casesplit-process-theorem (car theorems)
                                              pos old$ ctx state))
                  ((er (list hyps news))
                   (casesplit-process-theorems-aux (cdr theorems)
                                                   (1+ pos)
                                                   old$ ctx state)))
               (value (list (cons hyp hyps)
                            (cons new news))))))))

Function: casesplit-process-theorems

(defun casesplit-process-theorems
       (theorems old$ conditions$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old$)
                             (pseudo-term-listp conditions$))))
 (let ((__function__ 'casesplit-process-theorems))
  (declare (ignorable __function__))
  (b*
   (((unless (true-listp theorems))
     (er-soft+
      ctx t nil
      "The third input must be a true list, ~
                   but it is ~x0 instead."
      theorems))
    ((unless (= (len theorems)
                (1+ (len conditions$))))
     (er-soft+
      ctx t nil
      "The length of the third input must be ~
                   one plus the length ~x0 of the second input, ~
                   but it is ~x1 instead."
      (len conditions$)
      (len theorems)))
    (pos 1))
   (casesplit-process-theorems-aux theorems pos old$ ctx state))))