		Search-engine friendly clone of the ACL2 documentation.

Schemalg-input-processing

Schemalg-process-schema

Process the :schema input.

Signature
(schemalg-process-schema schema schema? ctx state) → (mv erp nothing state)
Arguments: schema? — Guard (booleanp schema?).
Returns: nothing — Type (null nothing).

Definitions and Theorems

Function: schemalg-process-schema

(defun schemalg-process-schema (schema schema? ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (booleanp schema?)))
 (let ((__function__ 'schemalg-process-schema))
  (declare (ignorable __function__))
  (if (member-eq schema *schemalg-schemas*)
      (value nil)
   (if schema?
    (er-soft+
     ctx t nil
     "The :SCHEMA input must be ~v0, ~
                   but it is ~x1 instead."
     *schemalg-schemas* schema)
    (er-soft+ ctx t nil
              "The :SCHEMA input must be supplied.")))))

Theorem: null-of-schemalg-process-schema.nothing

(defthm null-of-schemalg-process-schema.nothing
  (b* (((mv ?erp ?nothing acl2::?state)
        (schemalg-process-schema schema schema? ctx state)))
    (null nothing))
  :rule-classes :rewrite)