style: fix style in bv_decide normalizer (#5992)

Address comments by Markus in #5987
leanprover · Nov 7, 2024 · 17e6f3b · 17e6f3b
1 parent 5f7a40a
commit 17e6f3b
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -127,7 +127,7 @@ theorem BitVec.getElem_eq_getLsbD (a : BitVec w) (i : Nat) (h : i < w) :
     a[i]'h = a.getLsbD i := by
   simp [BitVec.getLsbD_eq_getElem?_getD, BitVec.getElem?_eq, h]
 
--- The side condition about gets resolved if i and w are constant.
+-- The side condition about being in bounds gets resolved if i and w are constant.
 attribute [bv_normalize] BitVec.getMsbD_eq_getLsbD
 
 end Reduce

diff --git a/tests/lean/run/bv_bitwise.lean b/tests/lean/run/bv_bitwise.lean
@@ -38,5 +38,5 @@ theorem bitwise_unit_9 (x y : BitVec 32) :
     BitVec.ofBool (x.getLsbD 0 ^^ y.getLsbD 0) = BitVec.ofBool ((x ^^^ y).getLsbD 0) := by
   bv_decide
 
-theorem bitwise_unit_10 (x : BitVec 2): (x.getMsbD 0) = x.msb := by
+theorem bitwise_unit_10 (x : BitVec 2) : (x.getMsbD 0) = x.msb := by
   bv_decide