		Search-engine friendly clone of the ACL2 documentation.

Atc-tag-tables

Atc-tag-info

Fixtype of information associated to an ACL2 defstruct symbol translated to a C structure type.

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

Fields

defstruct — defstruct-info
member-read-thms — symbol-list
member-write-thms — symbol-list

This consists of the information in the defstruct table plus some additional information that is more specific to ATC than to defstruct, which is part of the shallow embedding. This additional information consists of:

The names of the theorems generated by ATC for rewriting calls of exec-member and exec-memberp to calls of defstruct readers; see atc-gen-tag-member-read-all-thms.
The names of the theorems generated by ATC for rewriting calls of exec-expr on assignments with a :member or :memberp left expression to calls of defstruct writers; see atc-gen-tag-member-write-all-thms.

The latter theorems depend on exec-member, exec-memberp, and exec-expr, so they are not generated by defstruct to avoid having defstruct depend on those functions from the dynamic semantics.

Subtopics

Atc-tag-info-fix: Fixing function for atc-tag-info structures.
Atc-tag-info-equiv: Basic equivalence relation for atc-tag-info structures.
Make-atc-tag-info: Basic constructor macro for atc-tag-info structures.
Atc-tag-info->member-write-thms: Get the member-write-thms field from a atc-tag-info.
Atc-tag-info->member-read-thms: Get the member-read-thms field from a atc-tag-info.
Atc-tag-info->defstruct: Get the defstruct field from a atc-tag-info.
Change-atc-tag-info: Modifying constructor for atc-tag-info structures.
Atc-tag-infop: Recognizer for atc-tag-info structures.