		Search-engine friendly clone of the ACL2 documentation.

Defobject-implementation

Implementation of defobject.

Defobject-info: Fixtype of information about shallowly embedded external objects.
Defobject-gen-everything: Generate all the events.
Defobject-process-name: Process the name input.
Defobject-info-option: Fixtype of optional information about shallowly embedded C external objects.
Defobject-term-to-expr: Turn a constant expression term into the represented expression.
Term-checkers-common: Checkers of ACL2 terms that represent C constructs, common to ATC and defobject.
Defobject-process-init: Process the :init input.
Defobject-process-init-term: Process a term that is the :init input or an element of :init input.
Defobject-table-record-event: Event to update the table of shallowly embedded C external objects by recording a new C external object in it.
Defobject-process-type: Process the :type input.
Defobject-process-inputs: Process the inputs of defobject.
Defobject-table-lookup: Retrieve information about a shallowly embedded C external object.
Defobject-process-init-terms: Process the list :init.
Defobject-process-inputs-and-gen-everything: Process the inputs and generate the events.
Defobject-fn: Event expansion of defobject.
Defobject-table-definition: Definition of the table of shallowly embedded C external objects.
*defobject-table*: Name of the table of shallowly embedded external objects.
Defobject-macro-definition: Definition of defobject.