From 3843e10421cd424bfe43c45e1d25f6b515c4340b Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Fri, 4 Oct 2024 09:23:41 -0500 Subject: [PATCH] chore: bring back deleted text --- src/Init/Data/BitVec/Bitblast.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 825e8ed1dffd..4b75b8ec87d7 100644 --- 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,