From 3c53089d71a1b980b4485b991e4944a4d01bd8e9 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 18 Sep 2024 23:41:20 +0100 Subject: [PATCH] Drop unused lemmas --- src/Init/Data/BitVec/Lemmas.lean | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 748417f666c8..73994aeeff32 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -232,15 +232,6 @@ theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) := b theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b' ↔ b = b' := by decide -@[simp] theorem and_ofBool : ofBool a &&& ofBool b = ofBool (a && b) := by - cases a <;> cases b <;> rfl - -@[simp] theorem or_ofBool : ofBool a ||| ofBool b = ofBool (a || b) := by - cases a <;> cases b <;> rfl - -@[simp] theorem xor_ofBool : ofBool a ^^^ ofBool b = ofBool (a ^^ b) := by - cases a <;> cases b <;> rfl - @[simp] theorem not_ofBool : ~~~ (ofBool b) = ofBool (!b) := by cases b <;> rfl @[simp] theorem ofBool_and_ofBool : ofBool b &&& ofBool b' = ofBool (b && b') := by