Function vstd::std_specs::bits::u64_leading_zeros

source · 
pub open spec fn u64_leading_zeros(i: u64) -> int
Expand description
{ if i == 0 { 64 } else { u64_leading_zeros(i / 2) - 1 } }

Equivalent to i.leading_zeros(). See axiom_u64_leading_zeros for useful properties.