		Search-engine friendly clone of the ACL2 documentation.

Defmax-nat-implementation

Defmax-nat-fn

Process the inputs and generate the event to submit.

Signature
(defmax-nat-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: defmax-nat-fn

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