remove debug.byAsSorry

leanprover · Sep 2, 2024 · cdc99ce · cdc99ce
1 parent 1614885
commit cdc99ce
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -440,7 +440,6 @@ theorem msb_zeroExtend (x : BitVec w) : (x.zeroExtend v).msb = (decide (0 < v) &
 theorem msb_zeroExtend' (x : BitVec w) (h : w ≤ v) : (x.zeroExtend' h).msb = (decide (0 < v) && x.getLsb (v - 1)) := by
   rw [zeroExtend'_eq, msb_zeroExtend]
 
-set_option debug.byAsSorry true in
 /-- zero extending a bitvector to width 1 equals the boolean of the lsb. -/
 theorem zeroExtend_one_eq_ofBool_getLsb_zero (x : BitVec w) :
     x.zeroExtend 1 = BitVec.ofBool (x.getLsb 0) := by
@@ -457,7 +456,6 @@ theorem zeroExtend_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
   have hv := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi₁
   omega
 
-set_option debug.byAsSorry true in
 /-- Truncating to width 1 produces a bitvector equal to the least significant bit. -/
 theorem truncate_one {x : BitVec w} :
     x.truncate 1 = ofBool (x.getLsb 0) := by