bbv
bbv copied to clipboard
mit-plv
Bedrock Bit Vector Library
When trying to resintall coq-bbv.1.3 after upgrading coq in opam to 8.17.1, the following error is produced: ```shell File "./src/bbv/DepEq.v", line 17, characters 0-32: Error: The default value for rewriting...
Because of indices (which nest), every concrete 64 bit word has `2080` `S` constructors, even though it has only 64 `WS` constructors. Should we opt for a less intrinisically dependently...
It takes about 24 seconds on my machine, which is about 10% of the total time spent building util files in fiat-crypto (and is 1.5x slower than the next-slowest file)....
Since the generated Haskell does not import Data.Bits.testBit and Data.Char.ord, the overall compilation of the Haskell program fails. Any ideas to avoid generating these functions during Extraction?
Adapt to https://github.com/coq/coq/pull/19530 This is an adaptation in anticipation of the day the temporary backward compatibility introduced in the upstream PR will be removed (probably a few years in the...
