Skip to content

Commit 6878a2d

Browse files
committed
small change
1 parent 76b3e74 commit 6878a2d

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/Init/Data/BitVec/Lemmas.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1249,6 +1249,7 @@ theorem toNat_ushiftRight_eq_zero (x : BitVec w) (n : Nat) (hn : w ≤ n) :
12491249
theorem toInt_ushiftRight_zero (x : BitVec w) :
12501250
(x >>> 0).toInt = x.toInt := by simp
12511251

1252+
12521253
@[simp]
12531254
theorem toInt_ushiftRight_pos (x : BitVec w) (n : Nat) (hn : 0 < n) :
12541255
(x >>> n).toInt = x.toNat >>> n := by

0 commit comments

Comments
 (0)