		Search-engine friendly clone of the ACL2 documentation.

Schemalg-event-generation

Schemalg-gen-spec-1

Generate the function spec-1[?g1] or spec-1[?h].

Signature
(schemalg-gen-spec-1 schema spec-1 spec-1-enable old x-x1...xn x-a1...am x y iorel ?g1 ?h verify-guards wrld) → (mv local-event exported-event)
Arguments: schema — Guard (keywordp schema).; spec-1 — Guard (symbolp spec-1).; spec-1-enable — Guard (booleanp spec-1-enable).; old — Guard (symbolp old).; x-x1...xn — Guard (symbol-listp x-x1...xn).; x-a1...am — Guard (pseudo-term-listp x-a1...am).; x — Guard (symbolp x).; y — Guard (symbolp y).; iorel — Guard (pseudo-lambdap iorel).; ?g1 — Guard (symbolp ?g1).; ?h — Guard (symbolp ?h).; verify-guards — Guard (booleanp verify-guards).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.

Definitions and Theorems

Function: schemalg-gen-spec-1

(defun schemalg-gen-spec-1
       (schema spec-1
               spec-1-enable old x-x1...xn x-a1...am
               x y iorel ?g1 ?h verify-guards wrld)
 (declare (xargs :guard (and (keywordp schema)
                             (symbolp spec-1)
                             (booleanp spec-1-enable)
                             (symbolp old)
                             (symbol-listp x-x1...xn)
                             (pseudo-term-listp x-a1...am)
                             (symbolp x)
                             (symbolp y)
                             (pseudo-lambdap iorel)
                             (symbolp ?g1)
                             (symbolp ?h)
                             (booleanp verify-guards)
                             (plist-worldp wrld))))
 (let ((__function__ 'schemalg-gen-spec-1))
   (declare (ignorable __function__))
   (case schema
     (:divconq-list-0-1 (schemalg-gen-spec-1-divconq-list-0-1
                             spec-1
                             spec-1-enable old x-x1...xn x-a1...am
                             x y iorel ?h verify-guards wrld))
     (:divconq-list-0-1-2 (schemalg-gen-spec-1-divconq-list-0-1-2
                               spec-1
                               spec-1-enable old x-x1...xn x-a1...am
                               x iorel ?g1 verify-guards wrld))
     (:divconq-oset-0-1 (schemalg-gen-spec-1-divconq-oset-0-1
                             spec-1
                             spec-1-enable old x-x1...xn x-a1...am
                             x y iorel ?h verify-guards wrld))
     (t (prog2$ (raise "Internal error: unknown schema ~x0."
                       schema)
                (mv '(irrelevant) '(irrelevant)))))))