From 81a9bca6a0fc1cf52c688e4a438fd784bcacbb7d Mon Sep 17 00:00:00 2001 From: Siddharth Date: Wed, 25 Sep 2024 21:13:17 -0500 Subject: [PATCH] Update src/Init/Data/BitVec/Bitblast.lean Co-authored-by: Tobias Grosser --- src/Init/Data/BitVec/Bitblast.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index fb4962f97e06..4df79c838a49 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -535,7 +535,7 @@ structure DivModArgs (w : Nat) where /-- A `DivModState` is lawful if the remainder width `wr` plus the numerator width `wn` equals `w`, and the bitvectors `r` and `n` have values in the bounds given by bitwidths `wr`, resp. `wn`. -This is a proof engineering choice: An alternative world could have +This is a proof engineering choice: an alternative world could have been `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