		Search-engine friendly clone of the ACL2 documentation.

Schemalg-event-generation

Schemalg-gen-spec-0

Generate the function spec-0[?g] or spec-0[?g0].

Signature
(schemalg-gen-spec-0 schema spec-0 spec-0-enable old x-x1...xn x-a1...am x iorel ?g ?g0 verify-guards wrld) → (mv local-event exported-event)
Arguments: schema — Guard (keywordp schema).; spec-0 — Guard (symbolp spec-0).; spec-0-enable — Guard (booleanp spec-0-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).; iorel — Guard (pseudo-lambdap iorel).; ?g — Guard (symbolp ?g).; ?g0 — Guard (symbolp ?g0).; 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-0

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