Process the
(schemalg-process-cdr-output cdr-output cdr-output? schema old x-x1...xn ctx state) → (mv erp y state)
Function:
(defun schemalg-process-cdr-output (cdr-output cdr-output? schema old x-x1...xn ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (booleanp cdr-output?) (keywordp schema) (symbolp old) (symbol-listp x-x1...xn)))) (let ((__function__ 'schemalg-process-cdr-output)) (declare (ignorable __function__)) (b* ((schemas-allowed (list :divconq-list-0-1 :divconq-list-0-1-2)) ((when (and cdr-output? (not (member-eq schema schemas-allowed)))) (er-soft+ ctx t nil "The :CDR-OUTPUT input can be present only if ~ the :SCHEMA input is ~v0, but that input is ~x1 instead." schemas-allowed schema)) (y (if (eq cdr-output :auto) (intern-in-package-of-symbol "CDR-OUTPUT" old) cdr-output)) ((er &) (ensure-value-is-legal-variable-name$ y "The :CDR-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 :CDR-OUTPUT input" t nil))) (value y))))
Theorem:
(defthm symbolp-of-schemalg-process-cdr-output.y (b* (((mv ?erp ?y acl2::?state) (schemalg-process-cdr-output cdr-output cdr-output? schema old x-x1...xn ctx state))) (symbolp y)) :rule-classes :rewrite)