Function vstd::std_specs::bits::u16_leading_ones

source · 
pub open spec fn u16_leading_ones(i: u16) -> u32
Expand description
{ u16_leading_zeros(!i) }

Equivalent to i.leading_ones(). See axiom_u16_leading_ones for useful properties.