pub exec fn ex_u32_leading_zeros(i: u32) -> r : u32
Expand description
ensures
r == u32_leading_zeros(i),