coq/theories/Array, branch master The formal proof system Remove occurrences of Parray.reroot. 2020-10-08T09:16:48+00:00 Guillaume Melquiond 2020-08-31T06:52:05+00:00 e3764e1e857fce9b6d4cb018db676db3612c00a0 






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







Primitive persistent arrays
2020-07-06T09:22:43+00:00

Maxime Dénès

2020-02-03T17:19:42+00:00

0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6

Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.

Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>





Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.

Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>