diff options
Diffstat (limited to 'kernel/parray.mli')
| -rw-r--r-- | kernel/parray.mli | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/kernel/parray.mli b/kernel/parray.mli new file mode 100644 index 0000000000..0276278bd0 --- /dev/null +++ b/kernel/parray.mli @@ -0,0 +1,36 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val max_length : Uint63.t + +type 'a t +val length : 'a t -> Uint63.t +val length_int : 'a t -> int +val get : 'a t -> Uint63.t -> 'a +val set : 'a t -> Uint63.t -> 'a -> 'a t +val default : 'a t -> 'a +val make : Uint63.t -> 'a -> 'a t +val init : Uint63.t -> (int -> 'a) -> 'a -> 'a t +val copy : 'a t -> 'a t +val reroot : 'a t -> 'a t + +val map : ('a -> 'b) -> 'a t -> 'b t + +val to_array : 'a t -> 'a array * 'a (* default *) + +val of_array : 'a array -> 'a (* default *) -> 'a t + +val unsafe_of_array : 'a array -> 'a -> 'a t +(* [unsafe_of_array] injects a mutable array into a persistent one, but does + not perform a copy. This means that if the persistent array is mutated, the + original one will be too. *) + +val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a +val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a |