chore: add WIP to remind myself that I owe kim

opencompl · Sep 26, 2024 · 9055dc8 · 9055dc8
1 parent a6830f9
commit 9055dc8
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
@@ -26,6 +26,11 @@ expressions into expressions about individual bits in each vector.
 All other operations are to be PR'ed later and are already proved in
 https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean.
 
+### Example: How bitblasting work for multiplication
+
+- `succ`
+- `zero`
+
 -/
 
 set_option linter.missingDocs true