		Search-engine friendly clone of the ACL2 documentation.

Defobject-implementation

Defobject-fn

Event expansion of defobject.

Signature
(defobject-fn name type init call ctx state) → (mv erp event state)
Arguments: call — Guard (pseudo-event-formp call).; ctx — Guard (ctxp ctx).
Returns: event — A pseudo-event-formp.

Definitions and Theorems

Function: defobject-fn

(defun defobject-fn (name type init call ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (pseudo-event-formp call)
                              (ctxp ctx))))
  (let ((__function__ 'defobject-fn))
    (declare (ignorable __function__))
    (b* (((mv erp event)
          (defobject-process-inputs-and-gen-everything
               name type init call (w state)))
         ((when erp)
          (er-soft+ ctx t '(_) "~@0" erp)))
      (acl2::value event))))