		Search-engine friendly clone of the ACL2 documentation.

Specialize-event-generation

Specialize-gen-everything

Generate all the events.

Signature
(specialize-gen-everything code const-new target param const) → event
Arguments: code — Guard (code-ensemblep code).; const-new — Guard (symbolp const-new).; target — Guard (identp target).; param — Guard (identp param).; const — Guard (exprp const).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: specialize-gen-everything

(defun specialize-gen-everything (code const-new target param const)
  (declare (xargs :guard (and (code-ensemblep code)
                              (symbolp const-new)
                              (identp target)
                              (identp param)
                              (exprp const))))
  (b*
   ((code (specialize-code-ensemble code target param const))
    (defconst-event (cons 'defconst
                          (cons const-new
                                (cons (cons 'quote (cons code 'nil))
                                      'nil)))))
   defconst-event))

Theorem: pseudo-event-formp-of-specialize-gen-everything

(defthm pseudo-event-formp-of-specialize-gen-everything
 (b*
  ((event
     (specialize-gen-everything code const-new target param const)))
  (pseudo-event-formp event))
 :rule-classes :rewrite)