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 6edbfcd commit 83f382fCopy full SHA for 83f382f
src/Init/Data/BitVec/Lemmas.lean
@@ -5628,7 +5628,7 @@ theorem msb_replicate {n w : Nat} {x : BitVec w} :
5628
simp only [BitVec.msb, getMsbD_replicate, Nat.zero_mod]
5629
cases n <;> cases w <;> simp
5630
5631
-/-! ### Leading zeroes -/
+/-! ### Count leading zeroes -/
5632
5633
theorem clzAux_eq_zero_iff {x : BitVec w} {n : Nat} :
5634
clzAux x n = 0 ↔ x.getLsbD n = true := by
0 commit comments