From 59b70c52e7acf939221ddcb89bf405490ed56764 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 2 Sep 2024 16:53:15 +1000 Subject: [PATCH] remove debug.byAsSorry --- src/Init/Data/BitVec/Lemmas.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index f9c7f544b19b..234df0166ae3 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -529,7 +529,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.getLsbD (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.getLsbD 0) := by @@ -546,7 +545,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.getLsbD 0) := by