		Search-engine friendly clone of the ACL2 documentation.

Casesplit-implementation

Casesplit-fn

Check redundancy, process the inputs, and generate the event to submit.

Signature
(casesplit-fn old conditions theorems new-name new-enable thm-name thm-enable verify-guards hints print show-only call ctx state) → (mv erp event state)
Arguments: call — Guard (pseudo-event-formp call).
Returns: event — A pseudo-event-formp.

If this call to the transformation is redundant, a message to that effect is printed on the screen. If the transformation is redundant and :show-only is t, the encapsulate, retrieved from the table, is shown on the screen.

Definitions and Theorems

Function: casesplit-fn

(defun casesplit-fn (old conditions theorems new-name new-enable
                         thm-name thm-enable verify-guards
                         hints print show-only call ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (pseudo-event-formp call)))
  (let ((__function__ 'casesplit-fn))
    (declare (ignorable __function__))
    (b* ((encapsulate?
              (previous-transformation-expansion call (w state)))
         ((when encapsulate?)
          (b* (((run-when show-only)
                (cw "~x0~|" encapsulate?)))
            (cw "~%The transformation ~x0 is redundant.~%"
                call)
            (value '(value-triple :invisible))))
         ((er (list old$ conditions$ hyps
                    news new-name$ new-enable$ thm-name$
                    verify-guards$ hints$ names-to-avoid))
          (casesplit-process-inputs
               old
               conditions theorems new-name new-enable
               thm-name thm-enable verify-guards
               hints print show-only ctx state))
         ((er event)
          (casesplit-gen-everything
               old$
               conditions$ theorems hyps news new-name$
               new-enable$ thm-name$ thm-enable
               verify-guards$ hints$ print show-only
               call names-to-avoid ctx state)))
      (value event))))