package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
module type S = module type of Stdlib.Array
module type ExtS = sig ... end
include ExtS
include S
type !'a t = 'a array
val length : 'a array -> int
val get : 'a array -> int -> 'a
val set : 'a array -> int -> 'a -> unit
val make : int -> 'a -> 'a array
val create_float : int -> float array
val init : int -> (int -> 'a) -> 'a array
val make_matrix : int -> int -> 'a -> 'a array array
val append : 'a array -> 'a array -> 'a array
val concat : 'a array list -> 'a array
val sub : 'a array -> int -> int -> 'a array
val copy : 'a array -> 'a array
val fill : 'a array -> int -> int -> 'a -> unit
val blit : 'a array -> int -> 'a array -> int -> int -> unit
val to_list : 'a array -> 'a list
val of_list : 'a list -> 'a array
val iter : ('a -> unit) -> 'a array -> unit
val iteri : (int -> 'a -> unit) -> 'a array -> unit
val map : ('a -> 'b) -> 'a array -> 'b array
val map_inplace : ('a -> 'a) -> 'a array -> unit
val mapi : (int -> 'a -> 'b) -> 'a array -> 'b array
val mapi_inplace : (int -> 'a -> 'a) -> 'a array -> unit
val fold_left : ('acc -> 'a -> 'acc) -> 'acc -> 'a array -> 'acc
val fold_right : ('a -> 'acc -> 'acc) -> 'a array -> 'acc -> 'acc
val iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit
val map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
val for_all : ('a -> bool) -> 'a array -> bool
val exists : ('a -> bool) -> 'a array -> bool
val mem : 'a -> 'a array -> bool
val memq : 'a -> 'a array -> bool
val find_opt : ('a -> bool) -> 'a array -> 'a option
val find_index : ('a -> bool) -> 'a array -> int option
val find_map : ('a -> 'b option) -> 'a array -> 'b option
val find_mapi : (int -> 'a -> 'b option) -> 'a array -> 'b option
val combine : 'a array -> 'b array -> ('a * 'b) array
val sort : ('a -> 'a -> int) -> 'a array -> unit
val stable_sort : ('a -> 'a -> int) -> 'a array -> unit
val fast_sort : ('a -> 'a -> int) -> 'a array -> unit
val to_seq : 'a array -> 'a Stdlib.Seq.t
val to_seqi : 'a array -> (int * 'a) Stdlib.Seq.t
val of_seq : 'a Stdlib.Seq.t -> 'a array
val unsafe_get : 'a array -> int -> 'a
val unsafe_set : 'a array -> int -> 'a -> unit
module Floatarray : sig ... end
val compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int

First size comparison, then lexicographic order.

val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool

Lift equality to array type.

val equal_norefl : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool

Like equal but does not assume that equality is reflexive: no optimisation is performed if both arrays are physically the same.

val is_empty : 'a array -> bool

True whenever the array is empty.

val exists2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
val for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
val for_all3 : ('a -> 'b -> 'c -> bool) -> 'a array -> 'b array -> 'c array -> bool
val for_all4 : ('a -> 'b -> 'c -> 'd -> bool) -> 'a array -> 'b array -> 'c array -> 'd array -> bool
val for_all_i : (int -> 'a -> bool) -> int -> 'a array -> bool
val findi : (int -> 'a -> bool) -> 'a array -> int option
val hd : 'a array -> 'a

First element of an array, or Failure "Array.hd" if empty.

val tl : 'a array -> 'a array

Remaining part of hd, or Failure "Array.tl" if empty.

val last : 'a array -> 'a

Last element of an array, or Failure "Array.last" if empty.

val cons : 'a -> 'a array -> 'a array

Append an element on the left.

val rev : 'a array -> unit

In place reversal.

val fold_right_i : (int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a
val fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a
val fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c
val fold_right3 : ('a -> 'b -> 'c -> 'd -> 'd) -> 'a array -> 'b array -> 'c array -> 'd -> 'd
val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a
val fold_left4 : ('a -> 'b -> 'c -> 'd -> 'e -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'e array -> 'a
val fold_left2_i : (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
val fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
val map_to_list : ('a -> 'b) -> 'a array -> 'b list

Composition of map and to_list.

val map_of_list : ('a -> 'b) -> 'a list -> 'b array

Composition of map and of_list.

val chop : int -> 'a array -> 'a array * 'a array

chop i a returns (a1, a2) s.t. a = a1 + a2 and length a1 = n. Raise Failure "Array.chop" if i is not a valid index.

val split : ('a * 'b) array -> 'a array * 'b array
val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
val map3 : ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
val map3_i : (int -> 'a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
val map_left : ('a -> 'b) -> 'a array -> 'b array

As map but guaranteed to be left-to-right.

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

val fold_right_map : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c

Same, folding on the right

val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array

Same with two arrays, folding on the left; see also Smart.fold_left2_map

val fold_left2_map_i : (int -> 'a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array

Same than fold_left2_map but passing the index of the array

val fold_right2_map : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c

Same with two arrays, folding on the right

val distinct : 'a array -> bool

Return true if every element of the array is unique (for default equality).

val rev_of_list : 'a list -> 'a array

rev_of_list l is equivalent to Array.of_list (List.rev l).

val rev_to_list : 'a array -> 'a list

rev_to_list a is equivalent to List.rev (List.of_array a).

val filter_with : bool list -> 'a array -> 'a array

filter_with b a selects elements of a whose corresponding element in b is true. Raise Invalid_argument _ when sizes differ.

module Smart : sig ... end

The functions defined in this module are optimized specializations of the main ones, when the returned array is of same type as one of the original array.

module Fun1 : sig ... end

The functions defined in this module are the same as the main ones, except that they are all higher-order, and their function arguments have an additional parameter. This allows us to prevent closure creation in critical cases.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct