# Logops

Definitions and lemmas about logical operations on integers.

The books logops-definitions and logops-lemmas
contain a theory of the logical operations on numbers defined by CLTL (Section
12.7), and a portable implementation of the CLTL byte manipulation
functions (Section 12.8). These books also extend the CLTL logical operations
and byte manipulation theory with a few new definitions, lemmas supporting
those definitions, and useful macros.

These books were developed as a basis for the formal specification and
verification of hardware, where integers are used to represent binary signals
and busses. These books should be general enough, however, to be used as a
basis for reasoning about packed data structures, bit-encoded sets, and other
applications of logical operations on integers.

### Subtopics

- Logops-lemmas
- A book of lemmas about logical operations on numbers.