Update src/Init/Data/BitVec/Bitblast.lean

Co-authored-by: Alex Keizer <[email protected]>
opencompl · Sep 5, 2024 · f917a23 · f917a23
1 parent 29acadb
commit f917a23
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
@@ -519,7 +519,7 @@ This is a proof engineering choice: An alternative world could have
 `r : BitVec wr` and `n : BitVec wn`, but this required much more dependent typing coercions.
 
 Instead, we choose to declare all involved bitvectors as length `w`, and then prove that
-the values of `r` and `n` are within the bounds of `wr` and `wn` respectively.
+the values are within their respective bounds.
 -/
 structure DivModState.Lawful (w wr wn : Nat) (n d : BitVec w)
     (qr : DivModState w) : Prop where