		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-implementation

Deffoldred-fn

Event expansion of deffold-reduce.

Signature
(deffoldred-fn args ctx state) → (mv erp event state)
Arguments: args — Guard (true-listp args).; ctx — Guard (ctxp ctx).
Returns: event — Type (acl2::pseudo-event-formp event).

Definitions and Theorems

Function: deffoldred-fn

(defun deffoldred-fn (args ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp args) (ctxp ctx))))
 (let ((__function__ 'deffoldred-fn))
   (declare (ignorable __function__))
   (b*
    (((mv erp event)
      (deffoldred-process-inputs-and-gen-everything args (w state)))
     ((when erp)
      (acl2::er-soft+ ctx t '(_) "~@0" erp)))
    (value event))))

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

(defthm pseudo-event-formp-of-deffoldred-fn.event
  (b* (((mv ?erp acl2::?event acl2::?state)
        (deffoldred-fn args ctx state)))
    (acl2::pseudo-event-formp event))
  :rule-classes :rewrite)