coq 8.7.2 · OCaml Package

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 : int -> 'a -> 'a array

deprecated Use Array.make instead.

val create_float : int -> float array

val make_float : int -> float array

deprecated Use Array.create_float instead.

val init : int -> (int -> 'a) -> 'a array

val make_matrix : int -> int -> 'a -> 'a array array

val create_matrix : int -> int -> 'a -> 'a array array

deprecated Use Array.make_matrix instead.

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 mapi : (int -> 'a -> 'b) -> 'a array -> 'b array

val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a

val fold_right : ('b -> 'a -> 'a) -> 'b array -> 'a -> 'a

val mem : 'a -> 'a array -> bool

val memq : 'a -> 'a array -> bool

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 Seq.t

val to_seqi : 'a array -> (int * 'a) Seq.t

val of_seq : 'a 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

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

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

val is_empty : 'a array -> bool

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

val exists2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool

val for_all : ('a -> bool) -> 'a 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

val tl : 'a array -> 'a array

val last : 'a array -> 'a

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

val rev : 'a array -> unit

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_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_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

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

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

val smartmap : ('a -> 'a) -> 'a array -> 'a array

val smartfoldmap : ('r -> 'a -> 'r * 'a) -> 'r -> 'a array -> 'r * 'a array

val map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c 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 map_left : ('a -> 'b) -> 'a array -> 'b array

val iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit

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

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

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

val distinct : 'a array -> bool

val rev_of_list : 'a list -> 'a array

val rev_to_list : 'a array -> 'a list

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

package coq