Structs§
Traits§
- ExEq
- ExOrd
- ExPartial
Eq - ExPartial
Ord - OrdSpec
- OrdSpec
Impl - Partial
EqIs - Partial
EqSpec - Partial
EqSpec Impl - Partial
OrdIs - Partial
OrdSpec - Partial
OrdSpec Impl
Functions§
- _verus_
external_ ⚠fn_ specification_ 747__ 60__ 32_ bool_ 32_ as_ 32_ Partial Eq_ 32__ 60__ 32_ bool_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ eq - _verus_
external_ ⚠fn_ specification_ 748__ 60__ 32_ bool_ 32_ as_ 32_ Partial Eq_ 32__ 60__ 32_ bool_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ ne - _verus_
external_ ⚠fn_ specification_ 749__ 60__ 32_ f32_ 32_ as_ 32_ Partial Eq_ 32__ 60__ 32_ f32_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ eq - _verus_
external_ ⚠fn_ specification_ 750__ 60__ 32_ f32_ 32_ as_ 32_ Partial Eq_ 32__ 60__ 32_ f32_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ ne - _verus_
external_ ⚠fn_ specification_ 751__ 60__ 32_ f32_ 32_ as_ 32_ Partial Ord_ 32__ 60__ 32_ f32_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ partial__ cmp - _verus_
external_ ⚠fn_ specification_ 752__ 60__ 32_ f32_ 32_ as_ 32_ Partial Ord_ 32__ 60__ 32_ f32_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ lt - _verus_
external_ ⚠fn_ specification_ 753__ 60__ 32_ f32_ 32_ as_ 32_ Partial Ord_ 32__ 60__ 32_ f32_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ le - _verus_
external_ ⚠fn_ specification_ 754__ 60__ 32_ f32_ 32_ as_ 32_ Partial Ord_ 32__ 60__ 32_ f32_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ gt - _verus_
external_ ⚠fn_ specification_ 755__ 60__ 32_ f32_ 32_ as_ 32_ Partial Ord_ 32__ 60__ 32_ f32_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ ge - _verus_
external_ ⚠fn_ specification_ 756__ 60__ 32_ f64_ 32_ as_ 32_ Partial Eq_ 32__ 60__ 32_ f64_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ eq - _verus_
external_ ⚠fn_ specification_ 757__ 60__ 32_ f64_ 32_ as_ 32_ Partial Eq_ 32__ 60__ 32_ f64_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ ne - _verus_
external_ ⚠fn_ specification_ 758__ 60__ 32_ f64_ 32_ as_ 32_ Partial Ord_ 32__ 60__ 32_ f64_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ partial__ cmp - _verus_
external_ ⚠fn_ specification_ 759__ 60__ 32_ f64_ 32_ as_ 32_ Partial Ord_ 32__ 60__ 32_ f64_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ lt - _verus_
external_ ⚠fn_ specification_ 760__ 60__ 32_ f64_ 32_ as_ 32_ Partial Ord_ 32__ 60__ 32_ f64_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ le - _verus_
external_ ⚠fn_ specification_ 761__ 60__ 32_ f64_ 32_ as_ 32_ Partial Ord_ 32__ 60__ 32_ f64_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ gt - _verus_
external_ ⚠fn_ specification_ 762__ 60__ 32_ f64_ 32_ as_ 32_ Partial Ord_ 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