		Search-engine friendly clone of the ACL2 documentation.

Schemalg-input-processing

Schemalg-process-tail-output

Process the :tail-output input.

Signature
(schemalg-process-tail-output tail-output tail-output? schema old x-x1...xn ctx state) → (mv erp y state)
Arguments: tail-output? — Guard (booleanp tail-output?).; schema — Guard (keywordp schema).; old — Guard (symbolp old).; x-x1...xn — Guard (symbol-listp x-x1...xn).
Returns: y — Type (symbolp y).

Definitions and Theorems

Function: schemalg-process-tail-output

(defun schemalg-process-tail-output
       (tail-output tail-output?
                    schema old x-x1...xn ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp tail-output?)
                             (keywordp schema)
                             (symbolp old)
                             (symbol-listp x-x1...xn))))
 (let ((__function__ 'schemalg-process-tail-output))
  (declare (ignorable __function__))
  (b*
   ((schemas-allowed (list :divconq-oset-0-1))
    ((when (and tail-output?
                (not (member-eq schema schemas-allowed))))
     (er-soft+
      ctx t nil
      "The :TAIL-OUTPUT input can be present only if ~
                   the :SCHEMA input is ~v0, but that input is ~x1 instead."
      schemas-allowed schema))
    (y (if (eq tail-output :auto)
           (intern-in-package-of-symbol "TAIL-OUTPUT" old)
         tail-output))
    ((er &)
     (ensure-value-is-legal-variable-name$
          y "The :TAIL-OUTPUT input" t nil))
    ((er &)
     (ensure-value-is-not-in-list$
          y x-x1...xn
          (msg "one of bound variables ~x0 of ~x1"
               x-x1...xn old)
          "The :TAIL-OUTPUT input" t nil)))
   (value y))))

Theorem: symbolp-of-schemalg-process-tail-output.y

(defthm symbolp-of-schemalg-process-tail-output.y
  (b*
   (((mv ?erp ?y acl2::?state)
     (schemalg-process-tail-output tail-output tail-output?
                                   schema old x-x1...xn ctx state)))
   (symbolp y))
  :rule-classes :rewrite)