Word/bit-macros
Macros for manipulating integer words defined as contiguous bits.
These macros were defined to support the functions produced by
translating SPW .eqn files to ACL2 functions.
Subtopics
- Make-word-from-bits
- Update the low-order bits of word with the indicated values.
- Bind-word-to-bits
- Bind variables to the contiguous low-order bits of word.
