pub fn extern_spec_u8_trailing_zeros(self_: u8) -> u32Expand description
extern spec for u8::trailing_zeros
This is not a real function: its only use is for documentation.
ghost
ensures
#[logic_alias($type::trailing_zeros_logic)]pub fn extern_spec_u8_trailing_zeros(self_: u8) -> u32extern spec for u8::trailing_zeros
This is not a real function: its only use is for documentation.
ghost
ensures
#[logic_alias($type::trailing_zeros_logic)]