		Search-engine friendly clone of the ACL2 documentation.

Schemalg-event-generation

Schemalg-gen-new

Generate the function new.

Signature
(schemalg-gen-new new new-enable spec1...specq equal-algo verify-guards) → (mv local-event exported-event)
Arguments: new — Guard (symbolp new).; new-enable — Guard (booleanp new-enable).; spec1...specq — Guard (symbol-listp spec1...specq).; equal-algo — Guard (symbolp equal-algo).; verify-guards — Guard (booleanp verify-guards).
Returns: local-event — Type (pseudo-event-formp local-event).; exported-event — Type (pseudo-event-formp exported-event).

Definitions and Theorems

Function: schemalg-gen-new

(defun schemalg-gen-new (new new-enable
                             spec1...specq equal-algo verify-guards)
  (declare (xargs :guard (and (symbolp new)
                              (booleanp new-enable)
                              (symbol-listp spec1...specq)
                              (symbolp equal-algo)
                              (booleanp verify-guards))))
  (let ((__function__ 'schemalg-gen-new))
    (declare (ignorable __function__))
    (b* ((spec1...specq-calls
              (loop$ for spec
                     in spec1...specq collect (list spec))))
      (evmac-generate-soft-defun2
           new
           :formals nil
           :guard t
           :body (cons 'and
                       (cons (cons equal-algo 'nil)
                             spec1...specq-calls))
           :verify-guards verify-guards
           :enable new-enable
           :guard-hints '(("Goal" :in-theory nil))))))

Theorem: pseudo-event-formp-of-schemalg-gen-new.local-event

(defthm pseudo-event-formp-of-schemalg-gen-new.local-event
  (b* (((mv ?local-event ?exported-event)
        (schemalg-gen-new new new-enable spec1...specq
                          equal-algo verify-guards)))
    (pseudo-event-formp local-event))
  :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-schemalg-gen-new.exported-event

(defthm pseudo-event-formp-of-schemalg-gen-new.exported-event
  (b* (((mv ?local-event ?exported-event)
        (schemalg-gen-new new new-enable spec1...specq
                          equal-algo verify-guards)))
    (pseudo-event-formp exported-event))
  :rule-classes :rewrite)