chore: bring back deleted text

opencompl · Oct 4, 2024 · 3843e10 · 3843e10
1 parent 8378285
commit 3843e10
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
@@ -15,6 +15,9 @@ the `Fin 2^n` representation and Boolean vectors.  It is still under development
 intended to provide a path for converting SAT and SMT solver proofs about BitVectors
 as vectors of bits into proofs about Lean `BitVec` values.
 
+The module is named for the bit-blasting operation in an SMT solver that converts bitvector
+expressions into expressions about individual bits in each vector.
+
 ### Example: How bitblasting works for multiplication
 
 We explain how the lemmas here are used for bitblasting,