diff options
| author | Jason Gross | 2020-06-07 16:20:08 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-08-09 19:23:13 -0400 |
| commit | d39730a03b03bdbb23f0ad042a2bb87055d91d00 (patch) | |
| tree | 1680eafd043c2d0455a96011cea399d1ad950b2c /dev/include | |
| parent | ef08abec26c2f0017d1136870f8f99144e579538 (diff) | |
Bring Int63 notations into line with stdlib
We also put them in a module, so users can `Require Int63. Import
Int63.Int63Notations` without needing to unqualify the primitives.
In particular, we change
- `a \% m` into `a mod m` to correspond with the notation in ZArith
- `m == n` into `m =? n` to correspond with the eqb notations elsewhere
- `m < n` into `m <? n` to correspond with the ltb notations elsewhere
- `m <= n` into `m <=? n` to correspond with the leb notations elsewhere
- `m ≤ n` into `m ≤? n` for consistency with the non-unicode notation
The old notations are still accessible as deprecated notations.
Fixes #12454
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions