vstd_extra/external/
cmp.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Specifications for the free comparison functions missing from `vstd`.
3use vstd::{
4    prelude::*,
5    std_specs::cmp::{OrdSpec, PartialOrdSpec},
6};
7
8use core::cmp::Ordering;
9
10verus! {
11
12/// Returns `y` when it compares less than `x`, and returns `x` otherwise.
13pub open spec fn spec_ord_min<T: Ord>(x: T, y: T) -> T {
14    match y.cmp_spec(&x) {
15        Ordering::Less => y,
16        Ordering::Equal => x,
17        Ordering::Greater => x,
18    }
19}
20
21/// Returns `x` when `y` compares less than it, and returns `y` otherwise.
22pub open spec fn spec_ord_max<T: Ord>(x: T, y: T) -> T {
23    match y.cmp_spec(&x) {
24        Ordering::Less => x,
25        Ordering::Equal => y,
26        Ordering::Greater => y,
27    }
28}
29
30} // verus!
vstd_extra/external/cmp.rs

vstd_extra/external/
cmp.rs
