		Search-engine friendly clone of the ACL2 documentation.

Defmax-nat-input-processing

Defmax-nat-process-inputs

Process all the inputs.

Signature
(defmax-nat-process-inputs f y x1...xn body guard verify-guards ctx state) → (mv erp nothing state)
Returns: nothing — Type (null nothing).

We just check that the inputs have the right types. We do not check the body and guard inputs, since those are untranslated term, for which we do not quite have a ``type'' readily available.

Definitions and Theorems

Function: defmax-nat-process-inputs

(defun defmax-nat-process-inputs
       (f y x1...xn
          body guard verify-guards ctx state)
 (declare (xargs :stobjs (state)))
 (declare (ignore body guard))
 (declare (xargs :guard t))
 (let ((__function__ 'defmax-nat-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (ensure-value-is-symbol$ f "The first input" t nil))
    ((er &)
     (ensure-value-is-symbol$ y "The second input" t nil))
    ((er &)
     (ensure-value-is-symbol-list$ x1...xn "The third input" t nil))
    ((er &)
     (ensure-value-is-boolean$ verify-guards
                               "The :VERIFY-GUARDS input" t nil)))
   (value nil))))

Theorem: null-of-defmax-nat-process-inputs.nothing

(defthm null-of-defmax-nat-process-inputs.nothing
 (b*
  (((mv ?erp ?nothing ?state)
    (defmax-nat-process-inputs f y x1...xn
                               body guard verify-guards ctx state)))
  (null nothing))
 :rule-classes :rewrite)