		Search-engine friendly clone of the ACL2 documentation.

Tailrec-input-processing

Tailrec-process-variant

Process the variant input.

Signature
(tailrec-process-variant variant description error-erp error-val ctx state) → (mv erp val state)
Arguments: description — Guard (msgp description).; error-erp — Flag to return in case of error.; error-val — Value to return in case of error.; ctx — Context for errors.
Returns: erp — Type (implies erp (equal erp error-erp)).; val — Type (and (implies erp (equal val error-val)) (implies (and (not erp) error-erp) (not val))) .

Definitions and Theorems

Function: tailrec-process-variant

(defun tailrec-process-variant
       (variant description
                error-erp error-val ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (msgp description)))
  (b*
    (((unless (tailrec-variantp variant))
      (er-soft+
           ctx error-erp error-val
           "~@0 must be :MONOID, :MONOID-ALT, :ASSOC or :ASSOC-ALT."
           description)))
    (value nil)))

Theorem: return-type-of-tailrec-process-variant.erp

(defthm return-type-of-tailrec-process-variant.erp
  (b* (((mv ?erp ?val acl2::?state)
        (tailrec-process-variant variant description
                                 error-erp error-val ctx state)))
    (implies erp (equal erp error-erp)))
  :rule-classes :rewrite)

Theorem: return-type-of-tailrec-process-variant.val

(defthm return-type-of-tailrec-process-variant.val
  (b* (((mv ?erp ?val acl2::?state)
        (tailrec-process-variant variant description
                                 error-erp error-val ctx state)))
    (and (implies erp (equal val error-val))
         (implies (and (not erp) error-erp)
                  (not val))))
  :rule-classes :rewrite)

Subtopics

Tailrec-process-variant$: Calls tailrec-process-variant with ctx and state as the last two arguments.