From 32114ff99ff882d89525efbd78f965e3a7af20f0 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 16 Sep 2024 18:46:29 +1000 Subject: [PATCH] Update src/Init/Data/BitVec/Basic.lean --- src/Init/Data/BitVec/Basic.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index d0b4a7f08336..eb2b6986cb83 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -173,7 +173,6 @@ instance : GetElem (BitVec w) Nat Bool fun _ i => i < w where theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) : x[i] = x.toNat.testBit i := rfl -/-- This should become @[simp] after the getElem API has been completed. -/ theorem getLsbD_eq_getElem {x : BitVec w} {i : Nat} (h : i < w) : x.getLsbD i = x[i] := by simp [getLsbD, getElem_eq_testBit_toNat]