		Search-engine friendly clone of the ACL2 documentation.

Tailrec-input-processing

Tailrec-process-accumulator

Process the :accumulator input.

Signature
(tailrec-process-accumulator accumulator old$ r ctx state) → (mv erp a state)
Arguments: old$ — Guard (symbolp old$).; r — Guard (symbolp r).
Returns: a — Type (symbolp a).

Definitions and Theorems

Function: tailrec-process-accumulator

(defun tailrec-process-accumulator (accumulator old$ r ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old$) (symbolp r))))
 (let ((__function__ 'tailrec-process-accumulator))
  (declare (ignorable __function__))
  (if (eq accumulator :auto)
      (value (mbe :logic (acl2::symbol-fix r)
                  :exec r))
   (b*
    (((unless (legal-variablep accumulator))
      (er-soft+
       ctx t nil
       "The :ACCUMULATOR input must be a legal variable name,
                     but ~x0 is not a legal variable name."
       accumulator))
     (x1...xn (formals+ old$ (w state)))
     ((er &)
      (ensure-value-is-not-in-list$
           accumulator x1...xn
           (msg "one of the formal arguments ~&0 of ~x1"
                x1...xn old$)
           (msg "The :ACCUMULATOR input ~x0"
                accumulator)
           t nil)))
    (value accumulator)))))

Theorem: symbolp-of-tailrec-process-accumulator.a

(defthm symbolp-of-tailrec-process-accumulator.a
  (b* (((mv ?erp ?a acl2::?state)
        (tailrec-process-accumulator accumulator old$ r ctx state)))
    (symbolp a))
  :rule-classes :rewrite)