|
|
|---|
|
|
|
|---|
Fixtype of information associatated to an ACL2 variable translated to a C variable.
This is a product type introduced by fty::defprod.
For each variable, we store its C type, the name of a theorem about the variable, and a flag indicating whether the variable represents an external object (defined by a defobject).