		Search-engine friendly clone of the ACL2 documentation.

Solve-event-generation

Solve-gen-new

Generate the new function.

Signature
(solve-gen-new new new-enable x1...xn ?f f verify-guards print) → event
Arguments: new — Guard (symbolp new).; new-enable — Guard (booleanp new-enable).; x1...xn — Guard (symbol-listp x1...xn).; ?f — Guard (symbolp ?f).; f — Guard (symbolp f).; verify-guards — Guard (booleanp verify-guards).; print — Guard (evmac-input-print-p print).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: solve-gen-new

(defun solve-gen-new (new new-enable
                          x1...xn ?f f verify-guards print)
 (declare (xargs :guard (and (symbolp new)
                             (booleanp new-enable)
                             (symbol-listp x1...xn)
                             (symbolp ?f)
                             (symbolp f)
                             (booleanp verify-guards)
                             (evmac-input-print-p print))))
 (let ((__function__ 'solve-gen-new))
  (declare (ignorable __function__))
  (cons
   'soft::defequal
   (cons
    new
    (cons
     ':left
     (cons
      ?f
      (cons
       ':right
       (cons
        f
        (cons
         ':vars
         (cons
          x1...xn
          (cons
            ':enable
            (cons new-enable
                  (cons ':verify-guards
                        (cons verify-guards
                              (cons ':print
                                    (cons (and (eq print :all) :all)
                                          'nil))))))))))))))))

Theorem: pseudo-event-formp-of-solve-gen-new

(defthm pseudo-event-formp-of-solve-gen-new
  (b* ((event (solve-gen-new new new-enable
                             x1...xn ?f f verify-guards print)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)