		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-gen-everything

Event expansion of the transformation.

Signature
(simpadd0-gen-everything tunits-old const-new state) → (mv erp event)
Arguments: tunits-old — Guard (transunit-ensemblep tunits-old).; const-new — Guard (symbolp const-new).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: simpadd0-gen-everything

(defun simpadd0-gen-everything (tunits-old const-new state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (transunit-ensemblep tunits-old)
                              (symbolp const-new))))
  (declare
       (xargs :guard (and (transunit-ensemble-unambp tunits-old)
                          (transunit-ensemble-annop tunits-old))))
  (let ((__function__ 'simpadd0-gen-everything))
    (declare (ignorable __function__))
    (b* (((reterr) '(_))
         (gin (make-simpadd0-gin :const-new const-new
                                 :thm-index 1
                                 :names-to-avoid nil))
         ((mv tunits-new (simpadd0-gout gout))
          (simpadd0-transunit-ensemble tunits-old gin state))
         (const-event
              (cons 'defconst
                    (cons const-new
                          (cons (cons 'quote (cons tunits-new 'nil))
                                'nil)))))
      (retok (cons 'encapsulate
                   (cons 'nil
                         (cons const-event gout.events)))))))

Theorem: pseudo-event-formp-of-simpadd0-gen-everything.event

(defthm pseudo-event-formp-of-simpadd0-gen-everything.event
  (b* (((mv acl2::?erp acl2::?event)
        (simpadd0-gen-everything tunits-old const-new state)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)