Module vstd::std_specs::bits

Functions

• _verus_external_fn_specification_13_u8_32__58__58__32_trailing__zeros^⚠
• _verus_external_fn_specification_14_u8_32__58__58__32_trailing__ones^⚠
• _verus_external_fn_specification_15_u8_32__58__58__32_leading__zeros^⚠
• _verus_external_fn_specification_16_u8_32__58__58__32_leading__ones^⚠
• _verus_external_fn_specification_17_u16_32__58__58__32_trailing__zeros^⚠
• _verus_external_fn_specification_18_u16_32__58__58__32_trailing__ones^⚠
• _verus_external_fn_specification_19_u16_32__58__58__32_leading__zeros^⚠
• _verus_external_fn_specification_20_u16_32__58__58__32_leading__ones^⚠
• _verus_external_fn_specification_21_u32_32__58__58__32_trailing__zeros^⚠
• _verus_external_fn_specification_22_u32_32__58__58__32_trailing__ones^⚠
• _verus_external_fn_specification_23_u32_32__58__58__32_leading__zeros^⚠
• _verus_external_fn_specification_24_u32_32__58__58__32_leading__ones^⚠
• _verus_external_fn_specification_25_u64_32__58__58__32_trailing__zeros^⚠
• _verus_external_fn_specification_26_u64_32__58__58__32_trailing__ones^⚠
• _verus_external_fn_specification_27_u64_32__58__58__32_leading__zeros^⚠
• _verus_external_fn_specification_28_u64_32__58__58__32_leading__ones^⚠
• axiom_u8_leading_ones
• axiom_u8_leading_zeros
• axiom_u8_trailing_ones
• axiom_u8_trailing_zeros
• axiom_u16_leading_ones
• axiom_u16_leading_zeros
• axiom_u16_trailing_ones
• axiom_u16_trailing_zeros
• axiom_u32_leading_ones
• axiom_u32_leading_zeros
• axiom_u32_trailing_ones
• axiom_u32_trailing_zeros
• axiom_u64_leading_ones
• axiom_u64_leading_zeros
• axiom_u64_trailing_ones
• axiom_u64_trailing_zeros
• group_bits_axioms
• u8_leading_ones
• u8_leading_zeros
• u8_trailing_ones
• u8_trailing_zeros
• u16_leading_ones
• u16_leading_zeros
• u16_trailing_ones
• u16_trailing_zeros
• u32_leading_ones
• u32_leading_zeros
• u32_trailing_ones
• u32_trailing_zeros
• u64_leading_ones
• u64_leading_zeros
• u64_trailing_ones
• u64_trailing_zeros