diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-01 23:00:15 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-01 23:00:15 -0400 |
| commit | 68aca8687cd62127eb1dafa2029e59d38db68f3d (patch) | |
| tree | cdfcf85f2ffafea1dda2bf6ba26ab00ec4a48d3c /_CoqProject | |
| parent | d4f6f7373fc1f3a0ba1d1c17547f6d5b556bea5b (diff) | |
Fix definition of BoundedWord
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.
Diffstat (limited to '_CoqProject')
0 files changed, 0 insertions, 0 deletions