Process the
(schemalg-process-tail-output tail-output tail-output? schema old x-x1...xn ctx state) → (mv erp y state)
Function:
(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:
(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)