		Search-engine friendly clone of the ACL2 documentation.

Schemalg-input-processing

Schemalg-process-list-input

Process the :list-input input.

Signature
(schemalg-process-list-input list-input list-input? schema old ?f x-x1...xn x-a1...am ctx state) → (mv erp x state)
Arguments: list-input? — Guard (booleanp list-input?).; schema — Guard (keywordp schema).; old — Guard (symbolp old).; ?f — Guard (symbolp ?f).; x-x1...xn — Guard (symbol-listp x-x1...xn).; x-a1...am — Guard (pseudo-term-listp x-a1...am).
Returns: x — Type (symbolp x).

Definitions and Theorems

Function: schemalg-process-list-input

(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: symbolp-of-schemalg-process-list-input.x

(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)