From 1f3c265ef2b9ad81542320eae3f338bbd5432292 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 7 Nov 2024 12:37:48 +0100 Subject: [PATCH] style: fix style in bv_decide normalizer --- src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 2 +- tests/lean/run/bv_bitwise.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index a0eec2f76938..a7763e01f8d6 100644 --- 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 index 80a95febca5f..96923f7a12d7 100644 --- 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