vstd::std_specs::bits

Function u16_leading_zeros

Source 
pub closed spec fn u16_leading_zeros(i: u16) -> u32
Expand description

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