		Search-engine friendly clone of the ACL2 documentation.

Atc-event-and-code-generation

Atc-gen-thm-assert-events

Generate assertion events to double-check that all the correctness theorems were generated.

Signature
(atc-gen-thm-assert-events wf-thm fn-thms proofs) → events
Arguments: wf-thm — Guard (symbolp wf-thm).; fn-thms — Guard (symbol-symbol-alistp fn-thms).; proofs — Guard (booleanp proofs).
Returns: events — Type (pseudo-event-form-listp events).

This is to ensure that we do not accidentally miss the generation of some theorems.

We generate these assetions only if the :proofs input is t.

Definitions and Theorems

Function: atc-gen-thm-assert-events

(defun atc-gen-thm-assert-events (wf-thm fn-thms proofs)
 (declare (xargs :guard (and (symbolp wf-thm)
                             (symbol-symbol-alistp fn-thms)
                             (booleanp proofs))))
 (let ((__function__ 'atc-gen-thm-assert-events))
  (declare (ignorable __function__))
  (b*
   (((when (not proofs)) nil)
    (wf-thm-assert
         (cons 'assert-event
               (cons (cons 'theorem-symbolp
                           (cons (cons 'quote (cons wf-thm 'nil))
                                 '((w state))))
                     'nil)))
    (fn-thms-assert
     (loop$
      for
      fn-thm of-type cons in fn-thms collect
      (cons 'assert-event
            (cons (cons 'theorem-symbolp
                        (cons (cons 'quote (cons (cdr fn-thm) 'nil))
                              '((w state))))
                  'nil)))))
   (cons wf-thm-assert fn-thms-assert))))

Theorem: pseudo-event-form-listp-of-atc-gen-thm-assert-events

(defthm pseudo-event-form-listp-of-atc-gen-thm-assert-events
  (b* ((events (atc-gen-thm-assert-events wf-thm fn-thms proofs)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)