Module ops

Source

Traits§

Functions§

_verus_external_fn_specification_78__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_79__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_80__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_81__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_82__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_83__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_84__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_85__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_86__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_87__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_88__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_89__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_90__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_91__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_92__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_93__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_94__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_95__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_96__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_97__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_98__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_99__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_100__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_101__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_102__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_103__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_104__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_105__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_106__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_107__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_108__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_109__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_110__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_111__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_112__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_113__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_114__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_115__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_116__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_117__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_118__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_119__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_120__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_121__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_122__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_123__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_124__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_125__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_126__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_127__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_128__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_129__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_130__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_131__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_132__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_133__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_134__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_135__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_136__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_137__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_138__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_139__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_140__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_141__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_142__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_143__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_144__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_145__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_146__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_147__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_148__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_149__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_150__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_151__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_152__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_153__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_154__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_155__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_156__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_157__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_158__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_159__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_160__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_161__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_162__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_163__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_164__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_165__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_166__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_167__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_168__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_169__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_170__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_171__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_172__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_173__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_174__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_175__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_176__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_177__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_178__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_179__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_180__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_181__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_182__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_183__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_184__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_185__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_186__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_187__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_188__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_189__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_190__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_191__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_192__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_193__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_194__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_195__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_196__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_197__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_198__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_199__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_200__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_201__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_202__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_203__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_204__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_205__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_206__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_207__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_208__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_209__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_210__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_211__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_212__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_213__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_214__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_215__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_216__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_217__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_218__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_219__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_220__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_221__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_222__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_223__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_224__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_225__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_226__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_227__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 opsCopy item path

Traits§

Functions§

Module ops