		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-input-processing

Defarbrec-process-inputs

Process all the inputs.

Signature
(defarbrec-process-inputs fn x1...xn body update-names terminates-name measure-name nonterminating print show-only ctx state) → (mv erp result state)
Returns: result — A tuple (body$ test updates update-names$ terminates-name$ terminates-witness-name terminates-rewrite-name measure-name$ nonterminating$) satisfying (typed-tuplep pseudo-termp pseudo-termp pseudo-term-listp symbol-listp symbolp symbolp symbolp symbolp pseudo-termp result).

If validation is successful, return the results from the input validation functions called.

Definitions and Theorems

Function: defarbrec-process-inputs

(defun defarbrec-process-inputs
       (fn x1...xn
           body update-names terminates-name
           measure-name nonterminating
           print show-only ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'defarbrec-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (defarbrec-process-fn fn ctx state))
    ((er &)
     (defarbrec-process-x1...xn x1...xn ctx state))
    ((er (list body$ test updates))
     (defarbrec-process-body body fn x1...xn ctx state))
    ((er update-names$)
     (defarbrec-process-update-names
          update-names fn x1...xn ctx state))
    ((er (list terminates-name$ terminates-witness-name
               terminates-rewrite-name))
     (defarbrec-process-terminates-name terminates-name
                                        fn update-names$ ctx state))
    ((er measure-name$)
     (defarbrec-process-measure-name
          measure-name fn update-names$
          terminates-name$ terminates-witness-name
          terminates-rewrite-name ctx state))
    ((er nonterminating$)
     (defarbrec-process-nonterminating
          nonterminating x1...xn ctx state))
    ((er &)
     (defarbrec-process-print print ctx state))
    ((er &)
     (defarbrec-process-show-only show-only ctx state)))
   (value (list body$ test updates update-names$
                terminates-name$ terminates-witness-name
                terminates-rewrite-name
                measure-name$ nonterminating$)))))