Module cmp

Source

Traits§

ExEq
ExOrd
ExPartialEq
ExPartialOrd
OrdSpec
OrdSpecImpl
PartialEqIs
PartialEqSpec
PartialEqSpecImpl
PartialOrdIs
PartialOrdSpec
PartialOrdSpecImpl

Functions§

_verus_external_fn_specification_40__60__32_bool_32_as_32_PartialEq_32__60__32_bool_32__62__32__62__32__58__58__32_eq
_verus_external_fn_specification_41__60__32_bool_32_as_32_PartialEq_32__60__32_bool_32__62__32__62__32__58__58__32_ne
_verus_external_fn_specification_42__60__32_f32_32_as_32_PartialEq_32__60__32_f32_32__62__32__62__32__58__58__32_eq
_verus_external_fn_specification_43__60__32_f32_32_as_32_PartialEq_32__60__32_f32_32__62__32__62__32__58__58__32_ne
_verus_external_fn_specification_44__60__32_f32_32_as_32_PartialOrd_32__60__32_f32_32__62__32__62__32__58__58__32_partial__cmp
_verus_external_fn_specification_45__60__32_f32_32_as_32_PartialOrd_32__60__32_f32_32__62__32__62__32__58__58__32_lt
_verus_external_fn_specification_46__60__32_f32_32_as_32_PartialOrd_32__60__32_f32_32__62__32__62__32__58__58__32_le
_verus_external_fn_specification_47__60__32_f32_32_as_32_PartialOrd_32__60__32_f32_32__62__32__62__32__58__58__32_gt
_verus_external_fn_specification_48__60__32_f32_32_as_32_PartialOrd_32__60__32_f32_32__62__32__62__32__58__58__32_ge
_verus_external_fn_specification_49__60__32_f64_32_as_32_PartialEq_32__60__32_f64_32__62__32__62__32__58__58__32_eq
_verus_external_fn_specification_50__60__32_f64_32_as_32_PartialEq_32__60__32_f64_32__62__32__62__32__58__58__32_ne
_verus_external_fn_specification_51__60__32_f64_32_as_32_PartialOrd_32__60__32_f64_32__62__32__62__32__58__58__32_partial__cmp
_verus_external_fn_specification_52__60__32_f64_32_as_32_PartialOrd_32__60__32_f64_32__62__32__62__32__58__58__32_lt
_verus_external_fn_specification_53__60__32_f64_32_as_32_PartialOrd_32__60__32_f64_32__62__32__62__32__58__58__32_le
_verus_external_fn_specification_54__60__32_f64_32_as_32_PartialOrd_32__60__32_f64_32__62__32__62__32__58__58__32_gt
_verus_external_fn_specification_55__60__32_f64_32_as_32_PartialOrd_32__60__32_f64_32__62__32__62__32__58__58__32_ge
eq_ensures
ge_ensures
gt_ensures
le_ensures
lt_ensures
ne_ensures
partial_cmp_ensures