diff options
| author | coqbot-app[bot] | 2020-11-19 13:53:18 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-19 13:53:18 +0000 |
| commit | 01dea073194bf788414af549cc2753917540e964 (patch) | |
| tree | ff0e73bd0a51a4735a3e2a0dcc49477309020cbd /clib/cArray.mli | |
| parent | 7ebdf6bdbca2be4fc4ecddff0ac97bbb41c80cd0 (diff) | |
| parent | 73a2675e35b25c65582c02516943b0dd010016dd (diff) | |
Merge PR #12984: [printing] Order notations by matching precision first, and then by last imported
Reviewed-by: Zimmi48
Ack-by: RalfJung
Ack-by: gares
Diffstat (limited to 'clib/cArray.mli')
| -rw-r--r-- | clib/cArray.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/clib/cArray.mli b/clib/cArray.mli index f40ceb56db..664bad4c0a 100644 --- a/clib/cArray.mli +++ b/clib/cArray.mli @@ -92,6 +92,9 @@ sig val iter2_i : (int -> 'a -> 'b -> unit) -> 'a array -> 'b array -> unit (** Iter on two arrays. Raise [Invalid_argument "Array.iter2_i"] if sizes differ. *) + val iter3 : ('a -> 'b -> 'c -> unit) -> 'a array -> 'b array -> 'c array -> unit + (** Iter on three arrays. Raise [Invalid_argument "Array.iter3"] if sizes differ. *) + val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array (** [fold_left_map f e_0 [|l_1...l_n|] = e_n,[|k_1...k_n|]] where [(e_i,k_i)=f e_{i-1} l_i]; see also [Smart.fold_left_map] *) |