Process the
(schemalg-process-list-input list-input list-input? schema old ?f x-x1...xn x-a1...am ctx state) → (mv erp x state)
Function:
(defun schemalg-process-list-input (list-input list-input? schema old ?f x-x1...xn x-a1...am ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (booleanp list-input?) (keywordp schema) (symbolp old) (symbolp ?f) (symbol-listp x-x1...xn) (pseudo-term-listp x-a1...am)))) (let ((__function__ 'schemalg-process-list-input)) (declare (ignorable __function__)) (b* ((schemas-allowed (list :divconq-list-0-1 :divconq-list-0-1-2)) ((when (and list-input? (not (member-eq schema schemas-allowed)))) (er-soft+ ctx t nil "The :LIST-INPUT input can be present only if ~ the :SCHEMA input is ~v0, but that input is ~x1 instead." schemas-allowed schema))) (process-input-select-old-soft-io list-input :list-input old ?f x-x1...xn x-a1...am ctx state))))
Theorem:
(defthm symbolp-of-schemalg-process-list-input.x (b* (((mv ?erp ?x acl2::?state) (schemalg-process-list-input list-input list-input? schema old ?f x-x1...xn x-a1...am ctx state))) (symbolp x)) :rule-classes :rewrite)