From 9fc97da30c043adf561e12e732a3a80f0ad6fac0 Mon Sep 17 00:00:00 2001
From: Yan Peng <yppe@amazon.com>
Date: Tue, 1 Oct 2024 17:22:31 +0000
Subject: [PATCH] Adding back extractLsb lemmas in case we still need them

---
 Arm/BitVec.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean
index f971f09a..db872a56 100644
--- a/Arm/BitVec.lean
+++ b/Arm/BitVec.lean
@@ -59,7 +59,10 @@ attribute [bitvec_rules] BitVec.getLsbD_truncate
 attribute [bitvec_rules] BitVec.zeroExtend_zeroExtend_of_le
 attribute [bitvec_rules] BitVec.truncate_truncate_of_le
 attribute [bitvec_rules] BitVec.truncate_cast
+attribute [bitvec_rules] BitVec.extractLsb_ofFin
+attribute [bitvec_rules] BitVec.extractLsb_ofNat
 attribute [bitvec_rules] BitVec.extractLsb'_toNat
+attribute [bitvec_rules] BitVec.extractLsb_toNat
 attribute [bitvec_rules] BitVec.getLsbD_extract
 attribute [bitvec_rules] BitVec.toNat_allOnes
 attribute [bitvec_rules] BitVec.getLsbD_allOnes