Module ops

Source

Traits§

Functions§

_verus_external_fn_specification_443__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg^⚠
_verus_external_fn_specification_444__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg^⚠
_verus_external_fn_specification_445__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg^⚠
_verus_external_fn_specification_446__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg^⚠
_verus_external_fn_specification_447__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg^⚠
_verus_external_fn_specification_448__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg^⚠
_verus_external_fn_specification_449__60__32_bool_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not^⚠
_verus_external_fn_specification_450__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not^⚠
_verus_external_fn_specification_451__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not^⚠
_verus_external_fn_specification_452__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not^⚠
_verus_external_fn_specification_453__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not^⚠
_verus_external_fn_specification_454__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not^⚠
_verus_external_fn_specification_455__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not^⚠
_verus_external_fn_specification_456__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not^⚠
_verus_external_fn_specification_457__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not^⚠
_verus_external_fn_specification_458__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not^⚠
_verus_external_fn_specification_459__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not^⚠
_verus_external_fn_specification_460__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not^⚠
_verus_external_fn_specification_461__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not^⚠
_verus_external_fn_specification_462__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add^⚠
_verus_external_fn_specification_463__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add^⚠
_verus_external_fn_specification_464__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add^⚠
_verus_external_fn_specification_465__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add^⚠
_verus_external_fn_specification_466__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add^⚠
_verus_external_fn_specification_467__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add^⚠
_verus_external_fn_specification_468__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add^⚠
_verus_external_fn_specification_469__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add^⚠
_verus_external_fn_specification_470__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add^⚠
_verus_external_fn_specification_471__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add^⚠
_verus_external_fn_specification_472__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add^⚠
_verus_external_fn_specification_473__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add^⚠
_verus_external_fn_specification_474__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_AddAssign_32__62__32__58__58__32_add__assign^⚠
_verus_external_fn_specification_475__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_AddAssign_32__62__32__58__58__32_add__assign^⚠
_verus_external_fn_specification_476__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_AddAssign_32__62__32__58__58__32_add__assign^⚠
_verus_external_fn_specification_477__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_AddAssign_32__62__32__58__58__32_add__assign^⚠
_verus_external_fn_specification_478__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_AddAssign_32__62__32__58__58__32_add__assign^⚠
_verus_external_fn_specification_479__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_AddAssign_32__62__32__58__58__32_add__assign^⚠
_verus_external_fn_specification_480__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_AddAssign_32__62__32__58__58__32_add__assign^⚠
_verus_external_fn_specification_481__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_AddAssign_32__62__32__58__58__32_add__assign^⚠
_verus_external_fn_specification_482__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_AddAssign_32__62__32__58__58__32_add__assign^⚠
_verus_external_fn_specification_483__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_AddAssign_32__62__32__58__58__32_add__assign^⚠
_verus_external_fn_specification_484__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_AddAssign_32__62__32__58__58__32_add__assign^⚠
_verus_external_fn_specification_485__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_AddAssign_32__62__32__58__58__32_add__assign^⚠
_verus_external_fn_specification_486__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub^⚠
_verus_external_fn_specification_487__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub^⚠
_verus_external_fn_specification_488__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub^⚠
_verus_external_fn_specification_489__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub^⚠
_verus_external_fn_specification_490__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub^⚠
_verus_external_fn_specification_491__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub^⚠
_verus_external_fn_specification_492__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub^⚠
_verus_external_fn_specification_493__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub^⚠
_verus_external_fn_specification_494__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub^⚠
_verus_external_fn_specification_495__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub^⚠
_verus_external_fn_specification_496__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub^⚠
_verus_external_fn_specification_497__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub^⚠
_verus_external_fn_specification_498__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_SubAssign_32__62__32__58__58__32_sub__assign^⚠
_verus_external_fn_specification_499__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_SubAssign_32__62__32__58__58__32_sub__assign^⚠
_verus_external_fn_specification_500__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_SubAssign_32__62__32__58__58__32_sub__assign^⚠
_verus_external_fn_specification_501__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_SubAssign_32__62__32__58__58__32_sub__assign^⚠
_verus_external_fn_specification_502__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_SubAssign_32__62__32__58__58__32_sub__assign^⚠
_verus_external_fn_specification_503__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_SubAssign_32__62__32__58__58__32_sub__assign^⚠
_verus_external_fn_specification_504__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_SubAssign_32__62__32__58__58__32_sub__assign^⚠
_verus_external_fn_specification_505__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_SubAssign_32__62__32__58__58__32_sub__assign^⚠
_verus_external_fn_specification_506__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_SubAssign_32__62__32__58__58__32_sub__assign^⚠
_verus_external_fn_specification_507__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_SubAssign_32__62__32__58__58__32_sub__assign^⚠
_verus_external_fn_specification_508__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_SubAssign_32__62__32__58__58__32_sub__assign^⚠
_verus_external_fn_specification_509__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_SubAssign_32__62__32__58__58__32_sub__assign^⚠
_verus_external_fn_specification_510__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul^⚠
_verus_external_fn_specification_511__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul^⚠
_verus_external_fn_specification_512__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul^⚠
_verus_external_fn_specification_513__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul^⚠
_verus_external_fn_specification_514__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul^⚠
_verus_external_fn_specification_515__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul^⚠
_verus_external_fn_specification_516__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul^⚠
_verus_external_fn_specification_517__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul^⚠
_verus_external_fn_specification_518__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul^⚠
_verus_external_fn_specification_519__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul^⚠
_verus_external_fn_specification_520__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul^⚠
_verus_external_fn_specification_521__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul^⚠
_verus_external_fn_specification_522__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_MulAssign_32__62__32__58__58__32_mul__assign^⚠
_verus_external_fn_specification_523__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_MulAssign_32__62__32__58__58__32_mul__assign^⚠
_verus_external_fn_specification_524__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_MulAssign_32__62__32__58__58__32_mul__assign^⚠
_verus_external_fn_specification_525__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_MulAssign_32__62__32__58__58__32_mul__assign^⚠
_verus_external_fn_specification_526__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_MulAssign_32__62__32__58__58__32_mul__assign^⚠
_verus_external_fn_specification_527__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_MulAssign_32__62__32__58__58__32_mul__assign^⚠
_verus_external_fn_specification_528__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_MulAssign_32__62__32__58__58__32_mul__assign^⚠
_verus_external_fn_specification_529__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_MulAssign_32__62__32__58__58__32_mul__assign^⚠
_verus_external_fn_specification_530__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_MulAssign_32__62__32__58__58__32_mul__assign^⚠
_verus_external_fn_specification_531__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_MulAssign_32__62__32__58__58__32_mul__assign^⚠
_verus_external_fn_specification_532__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_MulAssign_32__62__32__58__58__32_mul__assign^⚠
_verus_external_fn_specification_533__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_MulAssign_32__62__32__58__58__32_mul__assign^⚠
_verus_external_fn_specification_534__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div^⚠
_verus_external_fn_specification_535__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div^⚠
_verus_external_fn_specification_536__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div^⚠
_verus_external_fn_specification_537__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div^⚠
_verus_external_fn_specification_538__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div^⚠
_verus_external_fn_specification_539__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div^⚠
_verus_external_fn_specification_540__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_DivAssign_32__62__32__58__58__32_div__assign^⚠
_verus_external_fn_specification_541__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_DivAssign_32__62__32__58__58__32_div__assign^⚠
_verus_external_fn_specification_542__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_DivAssign_32__62__32__58__58__32_div__assign^⚠
_verus_external_fn_specification_543__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_DivAssign_32__62__32__58__58__32_div__assign^⚠
_verus_external_fn_specification_544__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_DivAssign_32__62__32__58__58__32_div__assign^⚠
_verus_external_fn_specification_545__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_DivAssign_32__62__32__58__58__32_div__assign^⚠
_verus_external_fn_specification_546__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div^⚠
_verus_external_fn_specification_547__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div^⚠
_verus_external_fn_specification_548__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div^⚠
_verus_external_fn_specification_549__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div^⚠
_verus_external_fn_specification_550__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div^⚠
_verus_external_fn_specification_551__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div^⚠
_verus_external_fn_specification_552__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_DivAssign_32__62__32__58__58__32_div__assign^⚠
_verus_external_fn_specification_553__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_DivAssign_32__62__32__58__58__32_div__assign^⚠
_verus_external_fn_specification_554__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_DivAssign_32__62__32__58__58__32_div__assign^⚠
_verus_external_fn_specification_555__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_DivAssign_32__62__32__58__58__32_div__assign^⚠
_verus_external_fn_specification_556__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_DivAssign_32__62__32__58__58__32_div__assign^⚠
_verus_external_fn_specification_557__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_DivAssign_32__62__32__58__58__32_div__assign^⚠
_verus_external_fn_specification_558__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem^⚠
_verus_external_fn_specification_559__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem^⚠
_verus_external_fn_specification_560__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem^⚠
_verus_external_fn_specification_561__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem^⚠
_verus_external_fn_specification_562__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem^⚠
_verus_external_fn_specification_563__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem^⚠
_verus_external_fn_specification_564__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_RemAssign_32__62__32__58__58__32_rem__assign^⚠
_verus_external_fn_specification_565__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_RemAssign_32__62__32__58__58__32_rem__assign^⚠
_verus_external_fn_specification_566__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_RemAssign_32__62__32__58__58__32_rem__assign^⚠
_verus_external_fn_specification_567__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_RemAssign_32__62__32__58__58__32_rem__assign^⚠
_verus_external_fn_specification_568__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_RemAssign_32__62__32__58__58__32_rem__assign^⚠
_verus_external_fn_specification_569__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_RemAssign_32__62__32__58__58__32_rem__assign^⚠
_verus_external_fn_specification_570__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem^⚠
_verus_external_fn_specification_571__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem^⚠
_verus_external_fn_specification_572__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem^⚠
_verus_external_fn_specification_573__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem^⚠
_verus_external_fn_specification_574__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem^⚠
_verus_external_fn_specification_575__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem^⚠
_verus_external_fn_specification_576__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_RemAssign_32__62__32__58__58__32_rem__assign^⚠
_verus_external_fn_specification_577__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_RemAssign_32__62__32__58__58__32_rem__assign^⚠
_verus_external_fn_specification_578__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_RemAssign_32__62__32__58__58__32_rem__assign^⚠
_verus_external_fn_specification_579__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_RemAssign_32__62__32__58__58__32_rem__assign^⚠
_verus_external_fn_specification_580__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_RemAssign_32__62__32__58__58__32_rem__assign^⚠
_verus_external_fn_specification_581__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_RemAssign_32__62__32__58__58__32_rem__assign^⚠
_verus_external_fn_specification_582__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand^⚠
_verus_external_fn_specification_583__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand^⚠
_verus_external_fn_specification_584__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand^⚠
_verus_external_fn_specification_585__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand^⚠
_verus_external_fn_specification_586__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand^⚠
_verus_external_fn_specification_587__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand^⚠
_verus_external_fn_specification_588__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand^⚠
_verus_external_fn_specification_589__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand^⚠
_verus_external_fn_specification_590__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand^⚠
_verus_external_fn_specification_591__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand^⚠
_verus_external_fn_specification_592__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand^⚠
_verus_external_fn_specification_593__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand^⚠
_verus_external_fn_specification_594__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAndAssign_32__62__32__58__58__32_bitand__assign^⚠
_verus_external_fn_specification_595__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAndAssign_32__62__32__58__58__32_bitand__assign^⚠
_verus_external_fn_specification_596__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAndAssign_32__62__32__58__58__32_bitand__assign^⚠
_verus_external_fn_specification_597__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAndAssign_32__62__32__58__58__32_bitand__assign^⚠
_verus_external_fn_specification_598__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAndAssign_32__62__32__58__58__32_bitand__assign^⚠
_verus_external_fn_specification_599__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAndAssign_32__62__32__58__58__32_bitand__assign^⚠
_verus_external_fn_specification_600__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAndAssign_32__62__32__58__58__32_bitand__assign^⚠
_verus_external_fn_specification_601__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAndAssign_32__62__32__58__58__32_bitand__assign^⚠
_verus_external_fn_specification_602__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAndAssign_32__62__32__58__58__32_bitand__assign^⚠
_verus_external_fn_specification_603__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAndAssign_32__62__32__58__58__32_bitand__assign^⚠
_verus_external_fn_specification_604__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAndAssign_32__62__32__58__58__32_bitand__assign^⚠
_verus_external_fn_specification_605__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAndAssign_32__62__32__58__58__32_bitand__assign^⚠
_verus_external_fn_specification_606__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor^⚠
_verus_external_fn_specification_607__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor^⚠
_verus_external_fn_specification_608__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor^⚠
_verus_external_fn_specification_609__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor^⚠
_verus_external_fn_specification_610__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor^⚠
_verus_external_fn_specification_611__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor^⚠
_verus_external_fn_specification_612__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor^⚠
_verus_external_fn_specification_613__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor^⚠
_verus_external_fn_specification_614__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor^⚠
_verus_external_fn_specification_615__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor^⚠
_verus_external_fn_specification_616__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor^⚠
_verus_external_fn_specification_617__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor^⚠
_verus_external_fn_specification_618__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOrAssign_32__62__32__58__58__32_bitor__assign^⚠
_verus_external_fn_specification_619__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOrAssign_32__62__32__58__58__32_bitor__assign^⚠
_verus_external_fn_specification_620__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOrAssign_32__62__32__58__58__32_bitor__assign^⚠
_verus_external_fn_specification_621__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOrAssign_32__62__32__58__58__32_bitor__assign^⚠
_verus_external_fn_specification_622__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOrAssign_32__62__32__58__58__32_bitor__assign^⚠
_verus_external_fn_specification_623__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOrAssign_32__62__32__58__58__32_bitor__assign^⚠
_verus_external_fn_specification_624__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOrAssign_32__62__32__58__58__32_bitor__assign^⚠
_verus_external_fn_specification_625__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOrAssign_32__62__32__58__58__32_bitor__assign^⚠
_verus_external_fn_specification_626__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOrAssign_32__62__32__58__58__32_bitor__assign^⚠
_verus_external_fn_specification_627__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOrAssign_32__62__32__58__58__32_bitor__assign^⚠
_verus_external_fn_specification_628__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOrAssign_32__62__32__58__58__32_bitor__assign^⚠
_verus_external_fn_specification_629__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOrAssign_32__62__32__58__58__32_bitor__assign^⚠
_verus_external_fn_specification_630__60__32_bool_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor^⚠
_verus_external_fn_specification_631__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor^⚠
_verus_external_fn_specification_632__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor^⚠
_verus_external_fn_specification_633__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor^⚠
_verus_external_fn_specification_634__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor^⚠
_verus_external_fn_specification_635__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor^⚠
_verus_external_fn_specification_636__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor^⚠
_verus_external_fn_specification_637__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor^⚠
_verus_external_fn_specification_638__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor^⚠
_verus_external_fn_specification_639__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor^⚠
_verus_external_fn_specification_640__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor^⚠
_verus_external_fn_specification_641__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor^⚠
_verus_external_fn_specification_642__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor^⚠
_verus_external_fn_specification_643__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXorAssign_32__62__32__58__58__32_bitxor__assign^⚠
_verus_external_fn_specification_644__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXorAssign_32__62__32__58__58__32_bitxor__assign^⚠
_verus_external_fn_specification_645__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXorAssign_32__62__32__58__58__32_bitxor__assign^⚠
_verus_external_fn_specification_646__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXorAssign_32__62__32__58__58__32_bitxor__assign^⚠
_verus_external_fn_specification_647__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXorAssign_32__62__32__58__58__32_bitxor__assign^⚠
_verus_external_fn_specification_648__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXorAssign_32__62__32__58__58__32_bitxor__assign^⚠
_verus_external_fn_specification_649__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXorAssign_32__62__32__58__58__32_bitxor__assign^⚠
_verus_external_fn_specification_650__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXorAssign_32__62__32__58__58__32_bitxor__assign^⚠
_verus_external_fn_specification_651__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXorAssign_32__62__32__58__58__32_bitxor__assign^⚠
_verus_external_fn_specification_652__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXorAssign_32__62__32__58__58__32_bitxor__assign^⚠
_verus_external_fn_specification_653__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXorAssign_32__62__32__58__58__32_bitxor__assign^⚠
_verus_external_fn_specification_654__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXorAssign_32__62__32__58__58__32_bitxor__assign^⚠
_verus_external_fn_specification_655__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl^⚠
_verus_external_fn_specification_656__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl^⚠
_verus_external_fn_specification_657__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl^⚠
_verus_external_fn_specification_658__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl^⚠
_verus_external_fn_specification_659__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl^⚠
_verus_external_fn_specification_660__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl^⚠
_verus_external_fn_specification_661__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl^⚠
_verus_external_fn_specification_662__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl^⚠
_verus_external_fn_specification_663__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl^⚠
_verus_external_fn_specification_664__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl^⚠
_verus_external_fn_specification_665__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl^⚠
_verus_external_fn_specification_666__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl^⚠
_verus_external_fn_specification_667__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShlAssign_32__62__32__58__58__32_shl__assign^⚠
_verus_external_fn_specification_668__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShlAssign_32__62__32__58__58__32_shl__assign^⚠
_verus_external_fn_specification_669__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShlAssign_32__62__32__58__58__32_shl__assign^⚠
_verus_external_fn_specification_670__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShlAssign_32__62__32__58__58__32_shl__assign^⚠
_verus_external_fn_specification_671__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShlAssign_32__62__32__58__58__32_shl__assign^⚠
_verus_external_fn_specification_672__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShlAssign_32__62__32__58__58__32_shl__assign^⚠
_verus_external_fn_specification_673__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShlAssign_32__62__32__58__58__32_shl__assign^⚠
_verus_external_fn_specification_674__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShlAssign_32__62__32__58__58__32_shl__assign^⚠
_verus_external_fn_specification_675__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShlAssign_32__62__32__58__58__32_shl__assign^⚠
_verus_external_fn_specification_676__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShlAssign_32__62__32__58__58__32_shl__assign^⚠
_verus_external_fn_specification_677__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShlAssign_32__62__32__58__58__32_shl__assign^⚠
_verus_external_fn_specification_678__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShlAssign_32__62__32__58__58__32_shl__assign^⚠
_verus_external_fn_specification_679__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr^⚠
_verus_external_fn_specification_680__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr^⚠
_verus_external_fn_specification_681__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr^⚠
_verus_external_fn_specification_682__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr^⚠
_verus_external_fn_specification_683__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr^⚠
_verus_external_fn_specification_684__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr^⚠
_verus_external_fn_specification_685__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr^⚠
_verus_external_fn_specification_686__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr^⚠
_verus_external_fn_specification_687__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr^⚠
_verus_external_fn_specification_688__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr^⚠
_verus_external_fn_specification_689__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr^⚠
_verus_external_fn_specification_690__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr^⚠
_verus_external_fn_specification_691__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShrAssign_32__62__32__58__58__32_shr__assign^⚠
_verus_external_fn_specification_692__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShrAssign_32__62__32__58__58__32_shr__assign^⚠
_verus_external_fn_specification_693__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShrAssign_32__62__32__58__58__32_shr__assign^⚠
_verus_external_fn_specification_694__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShrAssign_32__62__32__58__58__32_shr__assign^⚠
_verus_external_fn_specification_695__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShrAssign_32__62__32__58__58__32_shr__assign^⚠
_verus_external_fn_specification_696__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShrAssign_32__62__32__58__58__32_shr__assign^⚠
_verus_external_fn_specification_697__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShrAssign_32__62__32__58__58__32_shr__assign^⚠
_verus_external_fn_specification_698__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShrAssign_32__62__32__58__58__32_shr__assign^⚠
_verus_external_fn_specification_699__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShrAssign_32__62__32__58__58__32_shr__assign^⚠
_verus_external_fn_specification_700__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShrAssign_32__62__32__58__58__32_shr__assign^⚠
_verus_external_fn_specification_701__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShrAssign_32__62__32__58__58__32_shr__assign^⚠
_verus_external_fn_specification_702__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_ShrAssign_32__62__32__58__58__32_shr__assign^⚠
_verus_external_fn_specification_703__60__32_f32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg^⚠
_verus_external_fn_specification_704__60__32_f32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add^⚠
_verus_external_fn_specification_705__60__32_f32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub^⚠
_verus_external_fn_specification_706__60__32_f32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul^⚠
_verus_external_fn_specification_707__60__32_f32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div^⚠
_verus_external_fn_specification_708__60__32_f64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg^⚠
_verus_external_fn_specification_709__60__32_f64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add^⚠
_verus_external_fn_specification_710__60__32_f64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub^⚠
_verus_external_fn_specification_711__60__32_f64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul^⚠
_verus_external_fn_specification_712__60__32_f64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div^⚠
add_ensures
div_ensures
mul_ensures
neg_ensures
sub_ensures

Module ops

Module ops Copy item path

Traits§

Functions§

Module ops