Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix definition of BoundedWord | Jason Gross | 2017-04-01 |
| | | | | | | | We need to take log2, because wordT takes lg(wordsize). We need to pass None rather than Some, because None means "the original output type of the function we're reifying is a tuple of Z" (as opposed to a tuple of words), which is the situation we're in. | ||
* | Split off BoundedWord.v from IntegrationTest.v | Jason Gross | 2017-04-01 |