		Search-engine friendly clone of the ACL2 documentation.

Defmapping-event-generation

Defmapping-gen-print-result

Generate the events that print the result.

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

This refers to the :result value of the :print input. The result to print consists of the generated theorems. These theorems are printed only if :print is :result or :info or :all.

Definitions and Theorems

Function: defmapping-gen-print-result

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

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

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