From e854510448636faf2c7a6a3ce5d5e426c0ff912c Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Sat, 7 Dec 2024 23:12:59 -0800 Subject: [PATCH] tonat thms --- src/Init/Data/BitVec/Lemmas.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index d5327a79f620..1df30710ef8f 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3036,7 +3036,6 @@ theorem toNat_rotateRight {x : BitVec w} {r : Nat} : (x.rotateRight r).toNat = (x.toNat >>> (r % w)) ||| x.toNat <<< (w - r % w) % (2^w) := by simp only [rotateRight, rotateRightAux, toNat_shiftLeft, toNat_ushiftRight, toNat_or] - /- ## twoPow -/ theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by