coq/test-suite/primitive/uint63, branch master The formal proof system Put all Int63 primitives in a separate file 2020-12-02T08:26:53+00:00 Pierre Roux 2020-10-26T13:43:05+00:00 853b838681db635f51fc3c7ba3dfe26bc6712d72 Following a request from Pierre-Marie Pédrot in #13258 
Following a request from Pierre-Marie Pédrot in #13258
Bring Int63 notations into line with stdlib 2020-08-09T23:23:13+00:00 Jason Gross 2020-06-07T20:20:08+00:00 d39730a03b03bdbb23f0ad042a2bb87055d91d00 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 
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
Add tests for primitive floats 2019-11-01T09:20:15+00:00 Guillaume Bertholon 2018-07-16T11:30:37+00:00 1b0bd3a9e3a913a4928b68546a134a1a4448f9e8 Add utility ldexp and frexp functions to prevent dealing with the shift of ldshiftexp and frshiftexp everywhere. Also move primitive integer tests to place all primitive tests in the same directory. 
Add utility ldexp and frexp functions to prevent dealing with the shift of
ldshiftexp and frshiftexp everywhere.

Also move primitive integer tests to place all primitive tests in the
same directory.