diff options
| author | Kazuhiko Sakaguchi | 2019-08-27 17:59:49 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-12-11 14:26:52 +0100 |
| commit | 581c08d1b045dbf51418df17350c84fda4eada93 (patch) | |
| tree | 7ae7054da07de87580de174b5cdfe67cb9a3033e /mathcomp/algebra/ssrint.v | |
| parent | f0e9ca0a160fd11716cc759cab8c6cbcbf20a32d (diff) | |
Reorder the arguments of the comparison predicates in order.v
The comparison predicates (for nat, ordered types, ordered integral domains)
must have the following order of arguments:
- leP x y : le_xor_gt x y ... (x <= y) (y < x) ... .
- ltP x y : lt_xor_ge x y ... (y <= x) (x < y) ... .
- ltgtP x y : compare x y ... (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y) ... .
Diffstat (limited to 'mathcomp/algebra/ssrint.v')
0 files changed, 0 insertions, 0 deletions