		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-event-generation

Defarbrec-gen-extend-table

Generate the event that extends the defarbrec table.

Signature
(defarbrec-gen-extend-table fn$ x1...xn$ body$ update-names$ terminates-name$ measure-name$ call$ expansion) → event
Arguments: fn$ — Guard (symbolp fn$).; x1...xn$ — Guard (symbol-listp x1...xn$).; body$ — Guard (pseudo-termp body$).; update-names$ — Guard (symbol-listp update-names$).; terminates-name$ — Guard (symbolp terminates-name$).; measure-name$ — Guard (symbolp measure-name$).; call$ — Guard (pseudo-event-formp call$).; expansion — Guard (pseudo-event-formp expansion).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: defarbrec-gen-extend-table

(defun defarbrec-gen-extend-table
       (fn$ x1...xn$
            body$ update-names$ terminates-name$
            measure-name$ call$ expansion)
  (declare (xargs :guard (and (symbolp fn$)
                              (symbol-listp x1...xn$)
                              (pseudo-termp body$)
                              (symbol-listp update-names$)
                              (symbolp terminates-name$)
                              (symbolp measure-name$)
                              (pseudo-event-formp call$)
                              (pseudo-event-formp expansion))))
  (let ((__function__ 'defarbrec-gen-extend-table))
    (declare (ignorable __function__))
    (b* ((info (make-defarbrec-info :call$ call$
                                    :expansion expansion
                                    :x1...xn x1...xn$
                                    :body body$
                                    :update-fns update-names$
                                    :terminates-fn terminates-name$
                                    :measure-fn measure-name$)))
      (cons 'table
            (cons *defarbrec-table-name*
                  (cons (cons 'quote (cons fn$ 'nil))
                        (cons (cons 'quote (cons info 'nil))
                              'nil)))))))

Theorem: pseudo-event-formp-of-defarbrec-gen-extend-table

(defthm pseudo-event-formp-of-defarbrec-gen-extend-table
 (b*
  ((event
    (defarbrec-gen-extend-table fn$ x1...xn$
                                body$ update-names$ terminates-name$
                                measure-name$ call$ expansion)))
  (pseudo-event-formp event))
 :rule-classes :rewrite)