		Search-engine friendly clone of the ACL2 documentation.

Casesplit-event-generation

Casesplit-gen-appconds-cond-guard

Generate the applicability conditions cond1-guard, ..., condp-guard, in that order.

Signature
(casesplit-gen-appconds-cond-guard old$ conditions$ state) → appconds
Arguments: old$ — Guard (symbolp old$).; conditions$ — Guard (pseudo-term-listp conditions$).
Returns: appconds — An evmac-appcond-listp.

Definitions and Theorems

Function: casesplit-gen-appconds-cond-guard-aux

(defun casesplit-gen-appconds-cond-guard-aux
       (k old$ conditions$ state acc)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (natp k)
                             (symbolp old$)
                             (pseudo-term-listp conditions$)
                             (symbol-alistp acc))))
 (declare (xargs :guard (<= k (len conditions$))))
 (let ((__function__ 'casesplit-gen-appconds-cond-guard-aux))
  (declare (ignorable __function__))
  (b*
   (((when (zp k)) acc)
    (appcond
        (casesplit-gen-appcond-cond-guard k old$ conditions$ state))
    (acc (cons appcond acc)))
   (casesplit-gen-appconds-cond-guard-aux
        (1- k)
        old$ conditions$ state acc))))

Function: casesplit-gen-appconds-cond-guard

(defun casesplit-gen-appconds-cond-guard (old$ conditions$ state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (symbolp old$)
                              (pseudo-term-listp conditions$))))
  (let ((__function__ 'casesplit-gen-appconds-cond-guard))
    (declare (ignorable __function__))
    (casesplit-gen-appconds-cond-guard-aux
         (len conditions$)
         old$ conditions$ state nil)))