From 11cd49c5f344944e51e328f1d594cbb93f37bded Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 17 Aug 2024 07:25:33 +0100 Subject: [PATCH] chore: drop BitVec over constant value rewrites --- SSA/Projects/InstCombine/ForLean.lean | 20 -------------------- 1 file changed, 20 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 7bb736533..701d41853 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -459,30 +459,10 @@ theorem toInt_width_zero (x : BitVec 0) : BitVec.toInt x = 0 := by rw [BitVec.width_zero_eq_zero x] simp -@[simp] -theorem toInt_ofInt_width_one_one : BitVec.toInt (BitVec.ofInt 1 1) = -1 := rfl - @[simp] theorem toInt_ofInt_zero : BitVec.toInt (BitVec.ofInt w 0) = 0 := by simp [BitVec.msb, BitVec.getMsb, BitVec.getLsb, BitVec.ofInt, BitVec.toInt] -@[simp] -theorem toInt_ofInt_1_width_zero : - BitVec.toInt (BitVec.ofInt (n := 0) 1) = 0 := rfl - -@[simp] -theorem toInt_ofInt_1_width_one : - BitVec.toInt (BitVec.ofInt (n := 1) 1) = -1 := rfl - --- if w = 0. then value is 0 --- if w = 1, then value is -1. - -@[simp] -theorem toNat_ofInt_one_width_zero : BitVec.toNat (BitVec.ofInt (n := 0) 1) = 0 := rfl - -@[simp] -theorem toNat_ofInt_one_width_one : BitVec.toNat (BitVec.ofInt (n := 1) 1) = 1 := rfl - @[simp] theorem ofNat_toNat_zero : BitVec.toNat (BitVec.ofInt w 0) = 0 := by