		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-implementation

Simpadd0-fn

Event expansion of simpadd0.

Signature
(simpadd0-fn const-old const-new proofs ctx state) → (mv erp event state)
Arguments: ctx — Guard (ctxp ctx).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: simpadd0-fn

(defun simpadd0-fn (const-old const-new proofs ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (ctxp ctx)))
  (let ((__function__ 'simpadd0-fn))
    (declare (ignorable __function__))
    (b* (((mv erp event)
          (simpadd0-process-inputs-and-gen-everything
               const-old const-new proofs (w state)))
         ((when erp)
          (er-soft+ ctx t '(_) "~@0" erp)))
      (value event))))

Theorem: pseudo-event-formp-of-simpadd0-fn.event

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