		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-event-generation

Defarbrec-gen-print-result

Generate the events that print the results.

Signature
(defarbrec-gen-print-result events) → cw-events
Arguments: events — Guard (pseudo-event-form-listp events).
Returns: cw-events — Type (pseudo-event-form-listp cw-events).

This is used when :print is :result or :all.

Definitions and Theorems

Function: defarbrec-gen-print-result

(defun defarbrec-gen-print-result (events)
  (declare (xargs :guard (pseudo-event-form-listp events)))
  (let ((__function__ 'defarbrec-gen-print-result))
    (declare (ignorable __function__))
    (if (endp events)
        nil
      (cons (cons 'cw-event
                  (cons '"~x0~|"
                        (cons (cons 'quote (cons (car events) 'nil))
                              'nil)))
            (defarbrec-gen-print-result (cdr events))))))

Theorem: pseudo-event-form-listp-of-defarbrec-gen-print-result

(defthm pseudo-event-form-listp-of-defarbrec-gen-print-result
  (b* ((cw-events (defarbrec-gen-print-result events)))
    (pseudo-event-form-listp cw-events))
  :rule-classes :rewrite)