# bbv - Bedrock Bit Vectors

Several Coq projects at MIT use a file called Word.v, defining bit vectors and lemmas about them.

This repo unifies the different versions of this file into one repository, so that everyone can benefit from additions made by other projects.

Suggested collaboration protocol:

-   For non-breaking, backwards-compatible (i.e. just additions) changes you just push to master, to keep the workflow as lightweight as possible.
-   For more "controversial" changes which might break something, make a PR.