lean-mlir
lean-mlir copied to clipboard
opencompl
Chore: prove that addition on BitStreams corresponds to Additon on BitVectors
There are currently two sorries in the file BitStream.lean. This proof removes one sorry, in the case of addition by proving that addition on BitVectors agrees with addition on BitStreams up to the first w bits.
![github-actions[bot] avatar](https://avatars.githubusercontent.com/in/15368?v=4 "Published by a pub.dev verified publisher"){kind=small}