vstd/std_specs/
cmp.rs

1use super::super::prelude::*;
2use super::borrow::BorrowSpec;
3
4use core::borrow::Borrow;
5use core::cmp::{Eq, Ord, Ordering, PartialEq, PartialOrd};
6use core::marker::PointeeSized;
7
8use verus as verus_skip_verusfmt;
9verus_skip_verusfmt! {
10
11#[verifier::external_trait_specification]
12#[verifier::external_trait_extension(PartialEqSpec via PartialEqSpecImpl)]
13pub trait ExPartialEq<Rhs: PointeeSized = Self>: PointeeSized {
14    type ExternalTraitSpecificationFor: PartialEq<Rhs>;
15
16    spec fn obeys_eq_spec() -> bool;
17
18    spec fn eq_spec(&self, other: &Rhs) -> bool;
19
20    fn eq(&self, other: &Rhs) -> (r: bool)
21        ensures
22            Self::obeys_eq_spec() ==> r == self.eq_spec(other);
23
24    fn ne(&self, other: &Rhs) -> (r: bool)
25        ensures
26            Self::obeys_eq_spec() ==> r == !self.eq_spec(other),
27        default_ensures
28            call_ensures(Self::eq, (self, other), !r);
29}
30
31#[verifier::external_trait_specification]
32pub trait ExEq: PartialEq + PointeeSized {
33    type ExternalTraitSpecificationFor: Eq;
34}
35
36#[verifier::external_type_specification]
37#[verifier::external_body]
38#[verifier::accept_recursive_types(T)]
39pub struct ExAssertParamIsEq<T: Eq + PointeeSized>(core::cmp::AssertParamIsEq<T>);
40
41#[verifier::external_trait_specification]
42#[verifier::external_trait_extension(PartialOrdSpec via PartialOrdSpecImpl)]
43pub trait ExPartialOrd<Rhs: PointeeSized = Self>: PartialEq<Rhs> + PointeeSized {
44    type ExternalTraitSpecificationFor: PartialOrd<Rhs>;
45
46    spec fn obeys_partial_cmp_spec() -> bool;
47
48    spec fn partial_cmp_spec(&self, other: &Rhs) -> Option<Ordering>;
49
50    fn partial_cmp(&self, other: &Rhs) -> (r: Option<Ordering>)
51        ensures
52            Self::obeys_partial_cmp_spec() ==> r == self.partial_cmp_spec(other);
53
54    fn lt(&self, other: &Rhs) -> (r: bool)
55        ensures
56            Self::obeys_partial_cmp_spec() ==>
57                (r <==> self.partial_cmp_spec(other) == Some(Ordering::Less)),
58        default_ensures
59            exists|o: Option<Ordering>|
60                {
61                    &&& #[trigger] call_ensures(Self::partial_cmp, (self, other), o)
62                    &&& r <==> o == Some(Ordering::Less)
63                }
64    ;
65
66    fn le(&self, other: &Rhs) -> (r: bool)
67        ensures
68            Self::obeys_partial_cmp_spec() ==>
69                (r <==> self.partial_cmp_spec(other) matches Some(
70                    Ordering::Less
71                    | Ordering::Equal,
72                )),
73        default_ensures
74            exists|o: Option<Ordering>|
75                {
76                    &&& #[trigger] call_ensures(Self::partial_cmp, (self, other), o)
77                    &&& r <==> o matches Some(
78                        Ordering::Less
79                        | Ordering::Equal,
80                    )
81                }
82    ;
83
84    fn gt(&self, other: &Rhs) -> (r: bool)
85        ensures
86            Self::obeys_partial_cmp_spec() ==>
87                (r <==> self.partial_cmp_spec(other) == Some(Ordering::Greater)),
88        default_ensures
89            exists|o: Option<Ordering>|
90                {
91                    &&& #[trigger] call_ensures(Self::partial_cmp, (self, other), o)
92                    &&& r <==> o == Some(Ordering::Greater)
93                }
94    ;
95
96    fn ge(&self, other: &Rhs) -> (r: bool)
97        ensures
98            Self::obeys_partial_cmp_spec() ==>
99                (r <==> self.partial_cmp_spec(other) matches Some(
100                    Ordering::Greater
101                    | Ordering::Equal,
102                )),
103        default_ensures
104            exists|o: Option<Ordering>|
105                {
106                    &&& #[trigger] call_ensures(Self::partial_cmp, (self, other), o)
107                    &&& r <==> o matches Some(
108                        Ordering::Greater
109                        | Ordering::Equal,
110                    )
111                }
112    ;
113}
114
115#[verifier::external_trait_specification]
116#[verifier::external_trait_extension(OrdSpec via OrdSpecImpl)]
117pub trait ExOrd: Eq + PartialOrd + PointeeSized {
118    type ExternalTraitSpecificationFor: Ord;
119
120    spec fn obeys_cmp_spec() -> bool;
121
122    spec fn cmp_spec(&self, other: &Self) -> Ordering;
123
124    fn cmp(&self, other: &Self) -> (r: Ordering)
125        ensures
126            Self::obeys_cmp_spec() ==> r == self.cmp_spec(other);
127
128    fn max(self, other: Self) -> (r: Self)
129        ensures
130            ({
131                &&& Self::obeys_cmp_spec()
132                &&& Self::obeys_partial_cmp_spec()
133                &&& other.partial_cmp_spec(&self) == Some(other.cmp_spec(&self))
134            }) ==> match other.cmp_spec(&self) {
135                Ordering::Less => r == self,
136                Ordering::Equal => r == other,
137                Ordering::Greater => r == other,
138            }
139        default_ensures
140            exists|b: bool|
141                {
142                    &&& #[trigger] call_ensures(Self::lt, (&other, &self), b)
143                    &&& b ==> r == self
144                    &&& !b ==> r == other
145                }
146    ;
147
148    fn min(self, other: Self) -> (r: Self)
149        ensures
150            ({
151                &&& Self::obeys_cmp_spec()
152                &&& Self::obeys_partial_cmp_spec()
153                &&& other.partial_cmp_spec(&self) == Some(other.cmp_spec(&self))
154            }) ==> match other.cmp_spec(&self) {
155                Ordering::Less => r == other,
156                Ordering::Equal => r == self,
157                Ordering::Greater => r == self,
158            }
159        default_ensures
160            exists|b: bool|
161                {
162                    &&& #[trigger] call_ensures(Self::lt, (&other, &self), b)
163                    &&& b ==> r == other
164                    &&& !b ==> r == self
165                }
166    ;
167
168    fn clamp(self, min: Self, max: Self) -> (r: Self)
169        requires
170            // There's an "assert!(min <= max)" in the provided clamp that must succeed, so:
171            Self::obeys_partial_cmp_spec(),
172            min.partial_cmp_spec(&max) matches Some(
173                Ordering::Less
174                | Ordering::Equal,
175            ),
176        ensures
177            ({
178                &&& Self::obeys_cmp_spec()
179                &&& Self::obeys_partial_cmp_spec()
180                &&& self.partial_cmp_spec(&min) == Some(self.cmp_spec(&min))
181                &&& self.partial_cmp_spec(&max) == Some(self.cmp_spec(&max))
182            }) ==> match (self.cmp_spec(&min), self.cmp_spec(&max)) {
183                (Ordering::Less, _) => r == min,
184                (_, Ordering::Greater) => r == max,
185                _ => r == self,
186            }
187        default_ensures
188            exists|b1: bool|
189                {
190                    &&& #[trigger] call_ensures(Self::lt, (&self, &min), b1)
191                    &&& b1 ==> r == min
192                    &&& !b1 ==> exists|b2: bool|
193                        {
194                            &&& #[trigger] call_ensures(Self::gt, (&self, &max), b2)
195                            &&& b2 ==> r == max
196                            &&& !b2 ==> r == self
197                        }
198                }
199    ;
200}
201
202/// Whether borrowing preserves the ordering of values.
203///
204/// This compares the `cmp_spec` results; faithfulness of the comparison and
205/// borrowing specifications is expressed separately by their `obeys_*_spec` predicates.
206pub open spec fn borrowed_key_ordering_matches<T: Borrow<U> + Ord, U: Ord + ?Sized>() -> bool {
207    forall|x: T, y: T| #[trigger]
208        x.cmp_spec(&y) == <T as BorrowSpec<U>>::borrow_spec(&x).cmp_spec(
209            <T as BorrowSpec<U>>::borrow_spec(&y),
210        )
211}
212
213pub trait PartialEqIs<Rhs: PointeeSized = Self>: PartialEq<Rhs> + PointeeSized {
214    spec fn is_eq(&self, other: &Rhs) -> bool;
215
216    spec fn is_ne(&self, other: &Rhs) -> bool;
217}
218
219pub trait PartialOrdIs<Rhs: PointeeSized = Self>: PartialOrd<Rhs> + PointeeSized {
220    spec fn is_lt(&self, other: &Rhs) -> bool;
221
222    spec fn is_le(&self, other: &Rhs) -> bool;
223
224    spec fn is_gt(&self, other: &Rhs) -> bool;
225
226    spec fn is_ge(&self, other: &Rhs) -> bool;
227}
228
229impl<A: PointeeSized + PartialEq<Rhs>, Rhs: PointeeSized> PartialEqIs<Rhs> for A {
230    #[verifier::inline]
231    open spec fn is_eq(&self, other: &Rhs) -> bool {
232        self.eq_spec(other)
233    }
234
235    #[verifier::inline]
236    open spec fn is_ne(&self, other: &Rhs) -> bool {
237        !self.eq_spec(other)
238    }
239}
240
241impl<A: PointeeSized + PartialOrd<Rhs>, Rhs: PointeeSized> PartialOrdIs<Rhs> for A {
242    #[verifier::inline]
243    open spec fn is_lt(&self, other: &Rhs) -> bool {
244        self.partial_cmp_spec(other) == Some(Ordering::Less)
245    }
246
247    #[verifier::inline]
248    open spec fn is_le(&self, other: &Rhs) -> bool {
249        matches!(self.partial_cmp_spec(other), Some(Ordering::Less | Ordering::Equal))
250    }
251
252    #[verifier::inline]
253    open spec fn is_gt(&self, other: &Rhs) -> bool {
254        self.partial_cmp_spec(other) == Some(Ordering::Greater)
255    }
256
257    #[verifier::inline]
258    open spec fn is_ge(&self, other: &Rhs) -> bool {
259        matches!(self.partial_cmp_spec(other), Some(Ordering::Greater | Ordering::Equal))
260    }
261}
262
263/* min and max */
264
265// `min` and `max` are aliases of `Ord::min` and `Ord::max`.
266pub assume_specification<T: Ord>[ core::cmp::min ](v1: T, v2: T) -> (r: T)
267    ensures
268        call_ensures(T::min, (v1, v2), r),
269;
270
271pub assume_specification<T: Ord>[ core::cmp::max ](v1: T, v2: T) -> (r: T)
272    ensures
273        call_ensures(T::max, (v1, v2), r),
274;
275
276// `min_by` and `max_by` call `compare(&v1, &v2)` once. When it returns `Equal`,
277// `min_by` returns `v1` and `max_by` returns `v2`.
278pub assume_specification<T, F: FnOnce(&T, &T) -> Ordering>[ core::cmp::min_by ](
279    v1: T,
280    v2: T,
281    compare: F,
282) -> (r: T)
283    requires
284        compare.requires((&v1, &v2)),
285    ensures
286        exists|o: Ordering| {
287            &&& #[trigger] compare.ensures((&v1, &v2), o)
288            &&& r == (if o == Ordering::Greater { v2 } else { v1 })
289        },
290;
291
292pub assume_specification<T, F: FnOnce(&T, &T) -> Ordering>[ core::cmp::max_by ](
293    v1: T,
294    v2: T,
295    compare: F,
296) -> (r: T)
297    requires
298        compare.requires((&v1, &v2)),
299    ensures
300        exists|o: Ordering| {
301            &&& #[trigger] compare.ensures((&v1, &v2), o)
302            &&& r == (if o == Ordering::Greater { v1 } else { v2 })
303        },
304;
305
306// `min_by_key` and `max_by_key` compute the keys `f(&v1)` and `f(&v2)` and
307// compare them with `<`. When neither key is less than the other, `min_by_key`
308// returns `v1` and `max_by_key` returns `v2`.
309pub assume_specification<T, F: FnMut(&T) -> K, K: Ord>[ core::cmp::min_by_key ](
310    v1: T,
311    v2: T,
312    f: F,
313) -> (r: T)
314    requires
315        f.requires((&v1,)),
316        f.requires((&v2,)),
317    ensures
318        exists|k1: K, k2: K, lt: bool| {
319            &&& f.ensures((&v1,), k1)
320            &&& f.ensures((&v2,), k2)
321            &&& #[trigger] call_ensures(K::lt, (&k2, &k1), lt)
322            &&& r == (if lt { v2 } else { v1 })
323        },
324;
325
326pub assume_specification<T, F: FnMut(&T) -> K, K: Ord>[ core::cmp::max_by_key ](
327    v1: T,
328    v2: T,
329    f: F,
330) -> (r: T)
331    requires
332        f.requires((&v1,)),
333        f.requires((&v2,)),
334    ensures
335        exists|k1: K, k2: K, lt: bool| {
336            &&& f.ensures((&v1,), k1)
337            &&& f.ensures((&v2,), k2)
338            &&& #[trigger] call_ensures(K::lt, (&k2, &k1), lt)
339            &&& r == (if lt { v1 } else { v2 })
340        },
341;
342
343/* bool */
344
345impl PartialEqSpecImpl for bool {
346    open spec fn obeys_eq_spec() -> bool {
347        true
348    }
349
350    open spec fn eq_spec(&self, other: &bool) -> bool {
351        *self == *other
352    }
353}
354
355pub assume_specification[ <bool as PartialEq<bool>>::eq ](x: &bool, y: &bool) -> bool;
356
357pub assume_specification[ <bool as PartialEq<bool>>::ne ](x: &bool, y: &bool) -> bool;
358
359/* char */
360
361impl PartialEqSpecImpl for char {
362    open spec fn obeys_eq_spec() -> bool {
363        true
364    }
365
366    open spec fn eq_spec(&self, other: &char) -> bool {
367        *self == *other
368    }
369}
370
371/* floating point */
372
373/*
374// Note: we do not assume that floating point types have obeys_*_spec() == true
375// because Rust floating point operations are not guaranteed to be deterministic.
376// (See https://github.com/rust-lang/rfcs/blob/master/text/3514-float-semantics.md )
377// Instead, we ensure an uninterpreted function about the result,
378// which can be used to trigger user-supplied axioms.
379*/
380
381pub uninterp spec fn eq_ensures<A>(x: A, y: A, o: bool) -> bool;
382
383pub uninterp spec fn ne_ensures<A>(x: A, y: A, o: bool) -> bool;
384
385pub uninterp spec fn partial_cmp_ensures<A>(x: A, y: A, o: Option<Ordering>) -> bool;
386
387pub uninterp spec fn lt_ensures<A>(x: A, y: A, o: bool) -> bool;
388
389pub uninterp spec fn le_ensures<A>(x: A, y: A, o: bool) -> bool;
390
391pub uninterp spec fn gt_ensures<A>(x: A, y: A, o: bool) -> bool;
392
393pub uninterp spec fn ge_ensures<A>(x: A, y: A, o: bool) -> bool;
394
395// Warning: floating-point eq is not the same as spec ==
396pub assume_specification[ <f32 as PartialEq<f32>>::eq ](x: &f32, y: &f32) -> (o: bool)
397    ensures
398        eq_ensures::<f32>(*x, *y, o),
399;
400
401// Warning: floating-point ne is not the same as spec !=
402pub assume_specification[ <f32 as PartialEq<f32>>::ne ](x: &f32, y: &f32) -> (o: bool)
403    ensures
404        ne_ensures::<f32>(*x, *y, o),
405;
406
407pub assume_specification[ <f32 as PartialOrd<f32>>::partial_cmp ](x: &f32, y: &f32) -> (o: Option<Ordering>)
408    ensures
409        partial_cmp_ensures::<f32>(*x, *y, o),
410;
411
412pub assume_specification[ <f32 as PartialOrd<f32>>::lt ](x: &f32, y: &f32) -> (o: bool)
413    ensures
414        lt_ensures::<f32>(*x, *y, o),
415;
416
417pub assume_specification[ <f32 as PartialOrd<f32>>::le ](x: &f32, y: &f32) -> (o: bool)
418    ensures
419        le_ensures::<f32>(*x, *y, o),
420;
421
422pub assume_specification[ <f32 as PartialOrd<f32>>::gt ](x: &f32, y: &f32) -> (o: bool)
423    ensures
424        gt_ensures::<f32>(*x, *y, o),
425;
426
427pub assume_specification[ <f32 as PartialOrd<f32>>::ge ](x: &f32, y: &f32) -> (o: bool)
428    ensures
429        ge_ensures::<f32>(*x, *y, o),
430;
431
432// Warning: floating-point eq is not the same as spec ==
433pub assume_specification[ <f64 as PartialEq<f64>>::eq ](x: &f64, y: &f64) -> (o: bool)
434    ensures
435        eq_ensures::<f64>(*x, *y, o),
436;
437
438// Warning: floating-point ne is not the same as spec !=
439pub assume_specification[ <f64 as PartialEq<f64>>::ne ](x: &f64, y: &f64) -> (o: bool)
440    ensures
441        ne_ensures::<f64>(*x, *y, o),
442;
443
444pub assume_specification[ <f64 as PartialOrd<f64>>::partial_cmp ](x: &f64, y: &f64) -> (o: Option<Ordering>)
445    ensures
446        partial_cmp_ensures::<f64>(*x, *y, o),
447;
448
449pub assume_specification[ <f64 as PartialOrd<f64>>::lt ](x: &f64, y: &f64) -> (o: bool)
450    ensures
451        lt_ensures::<f64>(*x, *y, o),
452;
453
454pub assume_specification[ <f64 as PartialOrd<f64>>::le ](x: &f64, y: &f64) -> (o: bool)
455    ensures
456        le_ensures::<f64>(*x, *y, o),
457;
458
459pub assume_specification[ <f64 as PartialOrd<f64>>::gt ](x: &f64, y: &f64) -> (o: bool)
460    ensures
461        gt_ensures::<f64>(*x, *y, o),
462;
463
464pub assume_specification[ <f64 as PartialOrd<f64>>::ge ](x: &f64, y: &f64) -> (o: bool)
465    ensures
466        ge_ensures::<f64>(*x, *y, o),
467;
468
469#[cfg(feature = "alloc")]
470impl<T: PartialEq + ?Sized, A: core::alloc::Allocator> PartialEqSpecImpl
471    for alloc::boxed::Box<T, A>
472{
473    open spec fn obeys_eq_spec() -> bool {
474        T::obeys_eq_spec()
475    }
476
477    open spec fn eq_spec(&self, other: &Self) -> bool {
478        <T as PartialEqSpec>::eq_spec(&**self, &**other)
479    }
480}
481
482/* reference types & */
483
484impl<A: PointeeSized, B: PointeeSized> PartialEqSpecImpl<&B> for &A
485where
486    A: PartialEq<B>,
487{
488    open spec fn obeys_eq_spec() -> bool {
489        <A as PartialEqSpec<B>>::obeys_eq_spec()
490    }
491
492    open spec fn eq_spec(&self, other: &&B) -> bool {
493        <A as PartialEqSpec<B>>::eq_spec(*self, *other)
494    }
495}
496
497pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialEq<&B>>::eq ](
498    a: &&'a A,
499    b: &&B,
500) -> bool
501where
502    A: PartialEq<B>,
503;
504
505pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialEq<&B>>::ne ](
506    a: &&'a A,
507    b: &&B,
508) -> bool
509where
510    A: PartialEq<B>,
511;
512
513impl<A: PointeeSized, B: PointeeSized> PartialOrdSpecImpl<&B> for &A
514where
515    A: PartialOrd<B>,
516{
517    open spec fn obeys_partial_cmp_spec() -> bool {
518        <A as PartialOrdSpec<B>>::obeys_partial_cmp_spec()
519    }
520
521    open spec fn partial_cmp_spec(&self, other: &&B) -> Option<core::cmp::Ordering> {
522        <A as PartialOrdSpec<B>>::partial_cmp_spec(*self, *other)
523    }
524}
525
526pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialOrd<&B>>::partial_cmp ](
527    a: &&'a A,
528    b: &&B,
529) -> Option<core::cmp::Ordering>
530where
531    A: PartialOrd<B>,
532;
533
534pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialOrd<&B>>::lt ](
535    a: &&'a A,
536    b: &&B,
537) -> bool
538where
539    A: PartialOrd<B>,
540;
541
542pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialOrd<&B>>::le ](
543    a: &&'a A,
544    b: &&B,
545) -> bool
546where
547    A: PartialOrd<B>,
548;
549
550pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialOrd<&B>>::gt ](
551    a: &&'a A,
552    b: &&B,
553) -> bool
554where
555    A: PartialOrd<B>,
556;
557
558pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialOrd<&B>>::ge ](
559    a: &&'a A,
560    b: &&B,
561) -> bool
562where
563    A: PartialOrd<B>,
564;
565
566impl<A: PointeeSized + Ord> OrdSpecImpl for &A {
567    open spec fn obeys_cmp_spec() -> bool {
568        A::obeys_cmp_spec()
569    }
570
571    open spec fn cmp_spec(&self, other: &Self) -> core::cmp::Ordering {
572        A::cmp_spec(*self, *other)
573    }
574}
575
576pub assume_specification<'a, A: PointeeSized + Ord>[ <&'a A as Ord>::cmp ](
577    a: &&'a A,
578    b: &&'a A,
579) -> core::cmp::Ordering
580;
581
582} // verus!
583
584macro_rules! tuple_cmp_impl {
585    ($($idx:tt $T:ident, )+) => {
586        verus! {
587        impl<$($T: PartialEq + PartialEqSpec),+> PartialEqSpecImpl for ($($T,)+)
588        {
589            open spec fn obeys_eq_spec() -> bool {
590                $(&&& $T::obeys_eq_spec())+
591            }
592
593            open spec fn eq_spec(&self, other: &($($T,)+)) -> bool {
594                $(&&& $T::eq_spec(&self.$idx, &other.$idx ))+
595            }
596        }
597
598        impl<$($T: PartialOrd + PartialOrdSpec),+> PartialOrdSpecImpl for ($($T,)+)
599        {
600            open spec fn obeys_partial_cmp_spec() -> bool {
601                $(&&& $T::obeys_partial_cmp_spec())+
602            }
603
604            open spec fn partial_cmp_spec(&self, other: &($($T,)+)) -> Option<core::cmp::Ordering> {
605                lexical_partial_cmp_spec!($( self.$idx, other.$idx ),+)
606            }
607        }
608
609        impl<$($T: Ord + OrdSpec),+> OrdSpecImpl for ($($T,)+)
610        {
611            open spec fn obeys_cmp_spec() -> bool {
612                $(&&& $T::obeys_cmp_spec())+
613            }
614
615            open spec fn cmp_spec(&self, other: &($($T,)+)) -> core::cmp::Ordering {
616                lexical_cmp_spec!($( self.$idx, other.$idx ),+)
617            }
618        }
619
620        }
621    };
622}
623
624#[allow(unused)]
625macro_rules! lexical_partial_cmp_spec {
626    ($a:expr, $b:expr, $($rest_a:expr, $rest_b:expr),+) => {
627        match ($a).partial_cmp_spec(&$b) {
628            Some(core::cmp::Ordering::Equal) => lexical_partial_cmp_spec!($($rest_a, $rest_b),+),
629            ordering => ordering
630        }
631    };
632    ($a:expr, $b:expr) => { ($a).partial_cmp_spec(&$b) };
633}
634
635#[allow(unused)]
636macro_rules! lexical_cmp_spec {
637    ($a:expr, $b:expr, $($rest_a:expr, $rest_b:expr),+) => {
638        match ($a).cmp_spec(&$b) {
639            core::cmp::Ordering::Equal => lexical_cmp_spec!($($rest_a, $rest_b),+),
640            ordering => ordering
641        }
642    };
643    ($a:expr, $b:expr) => { ($a).cmp_spec(&$b) };
644}
645
646tuple_cmp_impl!(0 T, );
647tuple_cmp_impl!(0 U, 1 T, );
648tuple_cmp_impl!(0 V, 1 U, 2 T, );
649tuple_cmp_impl!(0 W, 1 V, 2 U, 3 T, );
650tuple_cmp_impl!(0 X, 1 W, 2 V, 3 U, 4 T, );
651tuple_cmp_impl!(0 Y, 1 X, 2 W, 3 V, 4 U, 5 T, );
652tuple_cmp_impl!(0 Z, 1 Y, 2 X, 3 W, 4 V, 5 U, 6 T, );
653tuple_cmp_impl!(0 A, 1 Z, 2 Y, 3 X, 4 W, 5 V, 6 U, 7 T, );
654tuple_cmp_impl!(0 B, 1 A, 2 Z, 3 Y, 4 X, 5 W, 6 V, 7 U, 8 T, );
655tuple_cmp_impl!(0 C, 1 B, 2 A, 3 Z, 4 Y, 5 X, 6 W, 7 V, 8 U, 9 T, );
656tuple_cmp_impl!(0 D, 1 C, 2 B, 3 A, 4 Z, 5 Y, 6 X, 7 W, 8 V, 9 U, 10 T, );
657tuple_cmp_impl!(0 E, 1 D, 2 C, 3 B, 4 A, 5 Z, 6 Y, 7 X, 8 W, 9 V, 10 U, 11 T, );
vstd/std_specs/cmp.rs

vstd/std_specs/
cmp.rs
