Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | More lemmas about powers of 2 | Xavier Leroy | 2019-08-07 | 1 | -0/+14 |
| | |||||
* | Define integer sign extension for zero bits | Xavier Leroy | 2019-08-07 | 1 | -28/+30 |
| | | | | Just ensure sign_ext 0 x = zero. This simplifies some statements and proofs. | ||||
* | Zbits.v: add bit extraction and bit insertion | Xavier Leroy | 2019-08-07 | 1 | -0/+57 |
| | |||||
* | More efficient test for powers of two | Xavier Leroy | 2019-05-09 | 1 | -0/+83 |
| | | | | | | The previous implementation used to build the full powers-of-two decomposition of the number. The present implementation recognizes powers of two directly, then takes the log2. | ||||
* | Move Z definitions out of Integers and into Zbits | Xavier Leroy | 2019-04-26 | 1 | -0/+945 |
The module Integers.Make contained lots of definitions and theorems about Z integers that were independent of the word size. These definitions and theorems are useful outside Integers.Make, but it felt unnatural to fetch them from modules Int or Int64. This commit moves the word-size-independent definitions and theorems to a new module, lib/Zbits.v, and fixes their uses in the code base. |