		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-member-info

Fixtype of information about members of shallowly embedded C structures.

This is a product type introduced by fty::defprod.

Fields

memtype — member-type
reader — symbolp
reader-element — symbolp
writer — symbolp
writer-element — symbolp
checker — symbolp
length — symbolp
reader-return-thm — symbolp
reader-element-return-thm — symbolp
writer-return-thm — symbolp
writer-element-return-thm — symbolp

These are part of defstruct-info.

For each member, we store:

The member type, which consists of the name and type of the member. See member-type.
The name of the reader of the member. For an array member, this is the reader for the whole array.
The name of the reader of elements of an array member, which takes an index of any C integer type. This is nil for an integer member.
The name of the writer of the member. For an array member, this is the writer for the whole array.
The name of the writer of elements of an array member, which takes an index of any C integer type. This is nil for an integer member.
The name of the checker of indices of an array member, which takes indices of any C integer type. This is nil for an integer member.
The name of the length function of the member. This is nil except for a flexible array member.
The name of the return type theorem of the reader in reader.
The name of the return type theorem of the reader in reader-element. This is nil for an integer member.
The name of the return type theorem of the writer in writer.
The name of the return type theorem of the writer in writer-element. This is nil for an integer member.

Subtopics

Defstruct-member-info-fix: Fixing function for defstruct-member-info structures.
Make-defstruct-member-info: Basic constructor macro for defstruct-member-info structures.
Defstruct-member-info-equiv: Basic equivalence relation for defstruct-member-info structures.
Defstruct-member-infop: Recognizer for defstruct-member-info structures.
Defstruct-member-info->writer-element-return-thm: Get the writer-element-return-thm field from a defstruct-member-info.
Defstruct-member-info->reader-element-return-thm: Get the reader-element-return-thm field from a defstruct-member-info.
Change-defstruct-member-info: Modifying constructor for defstruct-member-info structures.
Defstruct-member-info->writer-return-thm: Get the writer-return-thm field from a defstruct-member-info.
Defstruct-member-info->reader-return-thm: Get the reader-return-thm field from a defstruct-member-info.
Defstruct-member-info->writer-element: Get the writer-element field from a defstruct-member-info.
Defstruct-member-info->reader-element: Get the reader-element field from a defstruct-member-info.
Defstruct-member-info->memtype: Get the memtype field from a defstruct-member-info.
Defstruct-member-info->writer: Get the writer field from a defstruct-member-info.
Defstruct-member-info->reader: Get the reader field from a defstruct-member-info.
Defstruct-member-info->length: Get the length field from a defstruct-member-info.
Defstruct-member-info->checker: Get the checker field from a defstruct-member-info.