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 f49e9bd commit a48535bCopy full SHA for a48535b
src/Init/Data/BitVec/Basic.lean
@@ -848,9 +848,7 @@ def smulOverflow {w : Nat} (x y : BitVec w) : Bool :=
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
851
- | n' + 1 =>
852
- if x.getLsbD n then 0
853
- else 1 + clzAux x n'
+ | n' + 1 => if x.getLsbD n then 0 else 1 + clzAux x n'
854
855
/-- Count the number of leading zeroes. -/
856
def clz {w : Nat} (x : BitVec w) : BitVec w := if w = 0 then 0 else BitVec.ofNat w (clzAux x (w - 1))
0 commit comments