Function vstd::std_specs::bits::ex_u64_leading_zeros

source · 
pub exec fn ex_u64_leading_zeros(i: u64) -> r : u32
Expand description
ensures
r as int == u64_leading_zeros(i),