Char-formats
Formats of (plain) char objects.
We formalize the possible formats of char objects,
along with some operations on them.
Subtopics
- Char-format->min
- The ACL2 integer value of CHAR_MIN [C17:5.2.4.2.1/1].
- Char-format->max
- The ACL2 integer value of CHAR_MAX [C17:5.2.4.2.1/1].
- Char-format
- Fixtype of formats of char objects.
- Char-format-8u
- The char format defined by 8 bits and unsignedness.
