Bool-format
Fixtype of formats of _Bool objects.
This is a product type introduced by fty::defprod.
Fields
- byte-size — posp
- value-index — natp
- trap — ACL2::any-p
[C17:6.2.5/2] says that _Bool is large enough to store 0 and 1.
[C17:6.2.5/6] classifies _Bool as an unsigned integer type;
as such, [C17:6.2.6.2/1] implies that _Bool object
must consist of value bits and padding bits.
Since only the values 0 and 1 are needed,
it seems reasonable to infer that _Bool objects
have exactly one value bit;
but since they must consist of an integral number of bytes [C17:6.2.6.1/2],
the rest must be all padding bits.
Although it does not seem reasonable to use more than one byte,
nothing seems to prevent _Bool object to take two or more bytes.
Thus, to capture the possible formats of _Bool objects,
we need the number of bytes (normally 1),
and the index of the value bit,
where the significance of the index is the same as
in the lists of bit roles in uinteger-format.
We also include information (for now unconstrained)
about possible trap representations [C17:6.2.6.1/5].
Subtopics
- Bool-format-fix
- Fixing function for bool-format structures.
- Bool-format-equiv
- Basic equivalence relation for bool-format structures.
- Make-bool-format
- Basic constructor macro for bool-format structures.
- Change-bool-format
- Modifying constructor for bool-format structures.
- Bool-format->value-index
- Get the value-index field from a bool-format.
- Bool-format->byte-size
- Get the byte-size field from a bool-format.
- Bool-format->trap
- Get the trap field from a bool-format.
- Bool-formatp
- Recognizer for bool-format structures.
