|
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
|
