		Search-engine friendly clone of the ACL2 documentation.

Defobject-implementation

Defobject-table-record-event

Event to update the table of shallowly embedded C external objects by recording a new C external object in it.

Signature
(defobject-table-record-event name info) → event
Arguments: name — Guard (stringp name).; info — Guard (defobject-infop info).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: defobject-table-record-event

(defun defobject-table-record-event (name info)
  (declare (xargs :guard (and (stringp name)
                              (defobject-infop info))))
  (let ((__function__ 'defobject-table-record-event))
    (declare (ignorable __function__))
    (cons 'table
          (cons *defobject-table*
                (cons name
                      (cons (cons 'quote (cons info 'nil))
                            'nil))))))

Theorem: pseudo-event-formp-of-defobject-table-record-event

(defthm pseudo-event-formp-of-defobject-table-record-event
  (b* ((event (defobject-table-record-event name info)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)