Fixtype of information associated to an ACL2 defstruct symbol translated to a C structure type.
This is a product type introduced by fty::defprod.
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 latter theorems depend on exec-member, exec-memberp, and exec-expr-asg, so they are not generated by defstruct to avoid having defstruct depend on those functions from the dynamic semantics.