		Search-engine friendly clone of the ACL2 documentation.

Defmin-int-implementation

Defmin-int-fn

Process the inputs and generate the event to submit.

Signature
(defmin-int-fn f y x1...xn body guard verify-guards ctx state) → (mv erp event state)
Returns: event — A pseudo-event-formp.

Definitions and Theorems

Function: defmin-int-fn

(defun defmin-int-fn (f y x1...xn
                        body guard verify-guards ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'defmin-int-fn))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (defmin-int-process-inputs f y x1...xn
                                body guard verify-guards ctx state))
    (event (defmin-int-gen-everything
                f y x1...xn body guard verify-guards)))
   (value event))))