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 dbc980f commit c38e2e1Copy full SHA for c38e2e1
src/Init/Data/BitVec/Basic.lean
@@ -842,9 +842,7 @@ treating `x` and `y` as 2's complement signed bitvectors.
842
def smulOverflow {w : Nat} (x y : BitVec w) : Bool :=
843
(x.toInt * y.toInt ≥ 2 ^ (w - 1)) || (x.toInt * y.toInt < - 2 ^ (w - 1))
844
845
-/--
846
- Count the number of leading zeros downward from the `n`-th bit to the `0`-th bit.
847
--/
+/-- Count the number of leading zeros downward from the `n`-th bit to the `0`-th bit. -/
848
def clzAux {w : Nat} (x : BitVec w) (n : Nat) : Nat :=
849
match n with
850
| 0 => if x.getLsbD 0 then 0 else 1
0 commit comments