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_ 246_ core_ 32__ 58__ 58__ 32_ cmp_ 32__ 58__ 58__ 32_ min - _verus_
external_ ⚠fn_ specification_ 247_ core_ 32__ 58__ 58__ 32_ cmp_ 32__ 58__ 58__ 32_ max - _verus_
external_ ⚠fn_ specification_ 248_ core_ 32__ 58__ 58__ 32_ cmp_ 32__ 58__ 58__ 32_ min__ by - _verus_
external_ ⚠fn_ specification_ 249_ core_ 32__ 58__ 58__ 32_ cmp_ 32__ 58__ 58__ 32_ max__ by - _verus_
external_ ⚠fn_ specification_ 250_ core_ 32__ 58__ 58__ 32_ cmp_ 32__ 58__ 58__ 32_ min__ by__ key - _verus_
external_ ⚠fn_ specification_ 251_ core_ 32__ 58__ 58__ 32_ cmp_ 32__ 58__ 58__ 32_ max__ by__ key - _verus_
external_ ⚠fn_ specification_ 252__ 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_ 253__ 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_ 254__ 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_ 255__ 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_ 256__ 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_ 257__ 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_ 258__ 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_ 259__ 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_ 260__ 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_ 261__ 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_ 262__ 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_ 263__ 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_ 264__ 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_ 265__ 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_ 266__ 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_ 267__ 60__ 32_ f64_ 32_ as_ 32_ Partial Ord_ 32__ 60__ 32_ f64_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ ge - _verus_
external_ ⚠fn_ specification_ 268__ 60__ 32__ 38__ 32__ 39_ a_ 32_ A_ 32_ as_ 32_ Partial Eq_ 32__ 60__ 32__ 38__ 32_ B_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ eq - _verus_
external_ ⚠fn_ specification_ 269__ 60__ 32__ 38__ 32__ 39_ a_ 32_ A_ 32_ as_ 32_ Partial Eq_ 32__ 60__ 32__ 38__ 32_ B_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ ne - _verus_
external_ ⚠fn_ specification_ 270__ 60__ 32__ 38__ 32__ 39_ a_ 32_ A_ 32_ as_ 32_ Partial Ord_ 32__ 60__ 32__ 38__ 32_ B_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ partial__ cmp - _verus_
external_ ⚠fn_ specification_ 271__ 60__ 32__ 38__ 32__ 39_ a_ 32_ A_ 32_ as_ 32_ Partial Ord_ 32__ 60__ 32__ 38__ 32_ B_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ lt - _verus_
external_ ⚠fn_ specification_ 272__ 60__ 32__ 38__ 32__ 39_ a_ 32_ A_ 32_ as_ 32_ Partial Ord_ 32__ 60__ 32__ 38__ 32_ B_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ le - _verus_
external_ ⚠fn_ specification_ 273__ 60__ 32__ 38__ 32__ 39_ a_ 32_ A_ 32_ as_ 32_ Partial Ord_ 32__ 60__ 32__ 38__ 32_ B_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ gt - _verus_
external_ ⚠fn_ specification_ 274__ 60__ 32__ 38__ 32__ 39_ a_ 32_ A_ 32_ as_ 32_ Partial Ord_ 32__ 60__ 32__ 38__ 32_ B_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ ge - _verus_
external_ ⚠fn_ specification_ 275__ 60__ 32__ 38__ 32__ 39_ a_ 32_ A_ 32_ as_ 32_ Ord_ 32__ 62__ 32__ 58__ 58__ 32_ cmp - borrowed_
key_ ordering_ matches - eq_
ensures - ge_
ensures - gt_
ensures - le_
ensures - lt_
ensures - ne_
ensures - partial_
cmp_ ensures