pub open spec fn u32_leading_ones(i: u32) -> u32
Expand description
{ u32_leading_zeros(!i) }
Equivalent to i.leading_ones()
.
See axiom_u32_leading_ones
for useful properties.
pub open spec fn u32_leading_ones(i: u32) -> u32
{ u32_leading_zeros(!i) }
Equivalent to i.leading_ones()
.
See axiom_u32_leading_ones
for useful properties.