		Search-engine friendly clone of the ACL2 documentation.

Defstruct

Defstruct-implementation

Implementation of defstruct.

Subtopics

Defstruct-info: Fixtype of information about shallowly embedded C structures.
Defstruct-gen-recognizer: Generate the recognizer of the structures defined by the defstruct.
Defstruct-gen-integer-member-ops: Generate the operations for an integer member of the structures defined by the defstruct.
Defstruct-gen-constructor: Generate the constructor of values of the structure type.
Defstruct-gen-array-member-ops: Generate the operations for an array member of the structures defined by defstruct.
Defstruct-gen-recognizer-conjuncts: Generate conjuncts for a member in the recognizer of the structures.
Defstruct-member-info: Fixtype of information about members of shallowly embedded C structures.
Defstruct-member-info-list->memtype-list: Lift defstruct-member-info->memtype to lists.
Defstruct-process-members: Process the member inputs of a defstruct call.
Defstruct-gen-fixer: Generate the fixer of the structures defined by the defstruct.
Defstruct-gen-member-ops: Generate the operations for a member of the structures defined by the defstruct.
Defstruct-process-inputs: Process the inputs of a defstruct call.
Defstruct-gen-fixing-term: Generate the fixing term for a member of a given type.
Defstruct-info-option: Fixtype of optional information about shallowly embedded C structures.
Defstruct-gen-everything: Generate all the events.
Defstruct-gen-all-member-ops: Generate the operations for all the members of the structures defined by the defstruct.
Defstruct-gen-recognizer-all-conjuncts: Generate conjuncts for all members in the recognizer of the structures.
Defstruct-info->writer-element-list: Collect all the writer-element components of a defstruct.
Defstruct-info->reader-element-list: Collect all the reader-element components of a defstruct.
Defstruct-gen-fixtype: Generate the fixtype of the structures defined by the defstruct.
Defstruct-info->writer-list: Collect all the writer components of a defstruct.
Defstruct-info->reader-list: Collect all the reader components of a defstruct.
Defstruct-fn: Process the inputs and generate the events.
Defstruct-table-record-event: Event to update the table of shallowly embedded C structures by recording a new C structure in it.
Defstruct-table-lookup: Retrieve information about a shallowly embedded C structure.
Irr-defstruct-info: Irrelevant information about a shallowly embedded C structure.
Defstruct-info->writer-element-list-aux
Defstruct-info->reader-element-list-aux
Defstruct-info->writer-list-aux
Defstruct-info->reader-list-aux
Defstruct-member-info-list: Fixtype of lists of information about members of shallowly embedded C structures.
Defstruct-table-definition: Definition of the table of shallowly embedded C structures.
*defstruct-table*: Name of the table of shallowly embedded C structures.
Defstruct-macro-implementtion: Definition of defstruct.