WIP

opencompl · Sep 18, 2024 · fee34f8 · fee34f8
1 parent 708b8a7
commit fee34f8
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -1443,6 +1443,7 @@ theorem toNat_cons' {x : BitVec w} :
 
 @[simp] theorem getElem_cons (b : Bool) {n} (x : BitVec n) (i : Nat) (h : i < 1 + n):
     (cons b x)[i] = if i = n then b else getLsbD x i := by
+
   stop
   simp only [getLsbD, toNat_cons, Nat.testBit_or]
   rw [Nat.testBit_shiftLeft]