		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-implementation

Deftreeops-process-inputs-and-gen-everything

Process the inputs and generate the events.

Signature
(deftreeops-process-inputs-and-gen-everything args call wrld) → (mv erp event)
Arguments: args — Guard (true-listp args).; call — Guard (pseudo-event-formp call).; wrld — Guard (plist-worldp wrld).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: deftreeops-process-inputs-and-gen-everything

(defun deftreeops-process-inputs-and-gen-everything (args call wrld)
 (declare (xargs :guard (and (true-listp args)
                             (pseudo-event-formp call)
                             (plist-worldp wrld))))
 (let ((__function__ 'deftreeops-process-inputs-and-gen-everything))
  (declare (ignorable __function__))
  (b* (((reterr) '(_))
       ((erp redundantp grammar rules prefix print)
        (deftreeops-process-inputs args call wrld))
       ((when redundantp)
        (retok '(value-triple :redundant))))
   (retok
     (deftreeops-gen-everything grammar rules prefix print call)))))

Theorem: pseudo-event-formp-of-deftreeops-process-inputs-and-gen-everything.event

(defthm
 pseudo-event-formp-of-deftreeops-process-inputs-and-gen-everything.event
 (b*
  (((mv acl2::?erp acl2::?event)
    (deftreeops-process-inputs-and-gen-everything args call wrld)))
  (pseudo-event-formp event))
 :rule-classes :rewrite)