We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 25de019 commit 261941dCopy full SHA for 261941d
src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -616,7 +616,7 @@ theorem or_mod_two_pow : (a ||| b) % 2 ^ n = a % 2 ^ n ||| b % 2 ^ n :=
616
617
@[simp, grind =] theorem testBit_xor (x y i : Nat) :
618
(x ^^^ y).testBit i = ((x.testBit i) ^^ (y.testBit i)) := by
619
- simp [HXor.hXor, XorOp.xor, xor, testBit_bitwise]
+ simp [HXor.hXor, XorOp.xor, xor, testBit_bitwise ]
620
621
@[simp, grind =] theorem zero_xor (x : Nat) : 0 ^^^ x = x := by
622
apply Nat.eq_of_testBit_eq
0 commit comments