		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-implementation

Defarbrec-fn

Check redundancy, process the inputs, and generate the event to submit.

Signature
(defarbrec-fn fn x1...xn body update-names terminates-name measure-name nonterminating print show-only call ctx state) → (mv erp event state)
Arguments: call — Guard (pseudo-event-formp call).
Returns: event — A pseudo-event-formp.

Definitions and Theorems

Function: defarbrec-fn

(defun defarbrec-fn (fn x1...xn
                        body update-names terminates-name
                        measure-name nonterminating
                        print show-only call ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (pseudo-event-formp call)))
 (let ((__function__ 'defarbrec-fn))
  (declare (ignorable __function__))
  (b*
   (((er redundant?)
     (defarbrec-check-redundancy fn print show-only call ctx state))
    ((when redundant?)
     (value '(value-triple :invisible)))
    ((er (list body$ test updates update-names$
               terminates-name$ teminates-witness-name$
               terminates-rewrite-name$
               measure-name$ nonterminating$))
     (defarbrec-process-inputs fn x1...xn
                               body update-names terminates-name
                               measure-name nonterminating
                               print show-only ctx state))
    (event (defarbrec-gen-everything
                fn
                x1...xn body$ test updates update-names$
                terminates-name$ teminates-witness-name$
                terminates-rewrite-name$
                measure-name$ nonterminating$
                print show-only call (w state))))
   (value event))))