		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-input-processing

Defarbrec-process-x1...xn

Process the (x1 ... xn) input.

Signature
(defarbrec-process-x1...xn x1...xn ctx state) → (mv erp nothing state)
Returns: nothing — Type (null nothing).

Definitions and Theorems

Function: defarbrec-process-x1...xn

(defun defarbrec-process-x1...xn (x1...xn ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'defarbrec-process-x1...xn))
  (declare (ignorable __function__))
  (b* ((description "The second input")
       ((er &)
        (ensure-value-is-symbol-list$ x1...xn description t nil))
       ((er &)
        (ensure-list-has-no-duplicates$ x1...xn description t nil)))
    (value nil))))

Theorem: null-of-defarbrec-process-x1...xn.nothing

(defthm null-of-defarbrec-process-x1...xn.nothing
  (b* (((mv ?erp ?nothing ?state)
        (defarbrec-process-x1...xn x1...xn ctx state)))
    (null nothing))
  :rule-classes :rewrite)