		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-implementation

Defdefparse-fn

Process the inputs and generate the events.

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

Definitions and Theorems

Function: defdefparse-fn

(defun defdefparse-fn (args call ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp args)
                             (pseudo-event-formp call)
                             (ctxp ctx))))
 (let ((__function__ 'defdefparse-fn))
  (declare (ignorable __function__))
  (b*
   (((when (defdefparse-table-lookup call (w state)))
     (value '(value-triple :redundant)))
    ((er (list name pkg-wit grammar prefix)
         :iferr '(_))
     (defdefparse-process-inputs args ctx state))
    (event
     (defdefparse-gen-everything name pkg-wit grammar prefix call)))
   (value event))))

Theorem: pseudo-event-formp-of-defdefparse-fn.even

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