Adding back extractLsb lemmas in case we still need them

pennyannn · Oct 1, 2024 · 9fc97da · 9fc97da
1 parent 1becfad
commit 9fc97da
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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