package coq-core

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a cmp = 'a -> 'a -> int
type 'a eq = 'a -> 'a -> bool
include module type of Stdlib.List
type !'a t = 'a list =
  1. | []
  2. | :: of 'a * 'a list
val length : 'a list -> int
val compare_lengths : 'a list -> 'b list -> int
val compare_length_with : 'a list -> int -> int
val cons : 'a -> 'a list -> 'a list
val hd : 'a list -> 'a
val tl : 'a list -> 'a list
val nth : 'a list -> int -> 'a
val nth_opt : 'a list -> int -> 'a option
val rev : 'a list -> 'a list
val rev_append : 'a list -> 'a list -> 'a list
val iter : ('a -> unit) -> 'a list -> unit
val iteri : (int -> 'a -> unit) -> 'a list -> unit
val mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
val rev_map : ('a -> 'b) -> 'a list -> 'b list
val filter_map : ('a -> 'b option) -> 'a list -> 'b list
val concat_map : ('a -> 'b list) -> 'a list -> 'b list
val fold_left : ('acc -> 'a -> 'acc) -> 'acc -> 'a list -> 'acc
val fold_right : ('a -> 'acc -> 'acc) -> 'a list -> 'acc -> 'acc
val iter2 : ('a -> 'b -> unit) -> 'a list -> 'b list -> unit
val rev_map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val fold_left2 : ('acc -> 'a -> 'b -> 'acc) -> 'acc -> 'a list -> 'b list -> 'acc
val fold_right2 : ('a -> 'b -> 'acc -> 'acc) -> 'a list -> 'b list -> 'acc -> 'acc
val for_all : ('a -> bool) -> 'a list -> bool
val exists : ('a -> bool) -> 'a list -> bool
val for_all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val exists2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val mem : 'a -> 'a list -> bool
val memq : 'a -> 'a list -> bool
val find : ('a -> bool) -> 'a list -> 'a
val find_opt : ('a -> bool) -> 'a list -> 'a option
val find_index : ('a -> bool) -> 'a list -> int option
val find_mapi : (int -> 'a -> 'b option) -> 'a list -> 'b option
val find_all : ('a -> bool) -> 'a list -> 'a list
val partition : ('a -> bool) -> 'a list -> 'a list * 'a list
val partition_map : ('a -> ('b, 'c) Stdlib.Either.t) -> 'a list -> 'b list * 'c list
val assoc : 'a -> ('a * 'b) list -> 'b
val assoc_opt : 'a -> ('a * 'b) list -> 'b option
val assq : 'a -> ('a * 'b) list -> 'b
val assq_opt : 'a -> ('a * 'b) list -> 'b option
val mem_assoc : 'a -> ('a * 'b) list -> bool
val mem_assq : 'a -> ('a * 'b) list -> bool
val remove_assoc : 'a -> ('a * 'b) list -> ('a * 'b) list
val remove_assq : 'a -> ('a * 'b) list -> ('a * 'b) list
val sort : ('a -> 'a -> int) -> 'a list -> 'a list
val stable_sort : ('a -> 'a -> int) -> 'a list -> 'a list
val fast_sort : ('a -> 'a -> int) -> 'a list -> 'a list
val sort_uniq : ('a -> 'a -> int) -> 'a list -> 'a list
val merge : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
val to_seq : 'a list -> 'a Stdlib.Seq.t
val of_seq : 'a Stdlib.Seq.t -> 'a list
Equality, testing
val compare : 'a cmp -> 'a list cmp

Lexicographic order on lists.

val equal : 'a eq -> 'a list eq

Lift equality to list type.

val is_empty : 'a list -> bool

Check whether a list is empty

val mem_f : 'a eq -> 'a -> 'a list -> bool

Same as List.mem, for some specific equality

val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool

Same as List.for_all but with an index

val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool

Same as List.for_all2 but returning false when of different length

val exists_i : (int -> 'a -> bool) -> int -> 'a list -> bool

Same as List.exists but with an index

val prefix_of : 'a eq -> 'a list eq

prefix_of eq l1 l2 returns true if l1 is a prefix of l2, false otherwise. It uses eq to compare elements

val same_length : 'a list -> 'b list -> bool

A more efficient variant of for_all2eq (fun _ _ -> true)

Creating lists
val interval : int -> int -> int list

interval i j creates the list [i; i + 1; ...; j], or [] when j <= i.

val make : int -> 'a -> 'a list

make n x returns a list made of n times x. Raise Invalid_argument _ if n is negative.

val addn : int -> 'a -> 'a list -> 'a list

addn n x l adds n times x on the left of l.

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

init n f constructs the list f 0; ... ; f (n - 1). Raise Invalid_argument _ if n is negative

val append : 'a list -> 'a list -> 'a list

Like OCaml's List.append but tail-recursive.

val concat : 'a list list -> 'a list

Like OCaml's List.concat but tail-recursive.

val flatten : 'a list list -> 'a list

Synonymous of concat

Lists as arrays
val assign : 'a list -> int -> 'a -> 'a list

assign l i x sets the i-th element of l to x, starting from 0. Raise Failure _ if i is out of range.

Filtering
val filter : ('a -> bool) -> 'a list -> 'a list

Like OCaml List.filter but tail-recursive and physically returns the original list if the predicate holds for all elements.

val filter2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list

Like List.filter but with 2 arguments, raise Invalid_argument _ if the lists are not of same length.

val filteri : (int -> 'a -> bool) -> 'a list -> 'a list

Like List.filter but with an index starting from 0

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

filter_with bl l selects elements of l whose corresponding element in bl is true. Raise Invalid_argument _ if sizes differ.

val map_filter : ('a -> 'b option) -> 'a list -> 'b list

Like map but keeping only non-None elements

val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list

Like map_filter but with an index starting from 0

val partitioni : (int -> 'a -> bool) -> 'a list -> 'a list * 'a list

Like List.partition but with an index starting from 0

Applying functorially
val map : ('a -> 'b) -> 'a list -> 'b list

Like OCaml List.map but tail-recursive

val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list

Like OCaml List.map2 but tail-recursive

val map_left : ('a -> 'b) -> 'a list -> 'b list

As map but ensures the left-to-right order of evaluation.

val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list

Like OCaml List.mapi but tail-recursive. Alternatively, like map but with an index

val map2_i : (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list

Like map2 but with an index

val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list

Like map but for 3 lists.

val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list

Like map but for 4 lists.

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

map_of_array f a behaves as List.map f (Array.to_list a)

val map_append : ('a -> 'b list) -> 'a list -> 'b list

map_append f [x1; ...; xn] returns f x1 @ ... @ f xn.

val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list

Like map_append but for two lists; raises Invalid_argument _ if the two lists do not have the same length.

val extend : bool list -> 'a -> 'a list -> 'a list

extend l a [a1..an] assumes that the number of true in l is n; it extends a1..an by inserting a at the position of false in l

val count : ('a -> bool) -> 'a list -> int

Count the number of elements satisfying a predicate

Finding position
val index : 'a eq -> 'a -> 'a list -> int

index returns the 1st index of an element in a list (counting from 1).

val safe_index : 'a eq -> 'a -> 'a list -> int option

safe_index returns the 1st index of an element in a list (counting from 1) and None otherwise.

val index0 : 'a eq -> 'a -> 'a list -> int

index0 behaves as index except that it starts counting at 0.

Folding
val fold_left_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a list -> 'c

acts like fold_left f acc s while f returns Cont acc'; it stops returning c as soon as f returns Stop c.

val fold_right_i : (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b

Like List.fold_right but with an index

val fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a

Like List.fold_left but with an index

val fold_right_and_left : ('b -> 'a -> 'a list -> 'b) -> 'a list -> 'b -> 'b

fold_right_and_left f [a1;...;an] hd is f (f (... (f (f hd an [an-1;...;a1]) an-1 [an-2;...;a1]) ...) a2 [a1]) a1 []

val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a

Like List.fold_left but for 3 lists; raise Invalid_argument _ if not all lists of the same size

val fold_left2_set : exn -> ('a -> 'b -> 'c -> 'b list -> 'c list -> 'a) -> 'a -> 'b list -> 'c list -> 'a

Fold sets, i.e. lists up to order; the folding function tells when elements match by returning a value and raising the given exception otherwise; sets should have the same size; raise the given exception if no pairing of the two sets is found;; complexity in O(n^2)

val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list

fold_left_map f e_0 [a1;...;an] is e_n,[k_1...k_n] where (e_i,k_i) is f e_{i-1} ai for each i<=n

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

Same, folding on the right

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

Same with two lists, folding on the left

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

Same with two lists, folding on the right

val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list

Same with three lists, folding on the left

val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list

Same with four lists, folding on the left

Splitting
val remove : 'a eq -> 'a -> 'a list -> 'a list

remove eq a l Remove all occurrences of a in l

val remove_first : ('a -> bool) -> 'a list -> 'a list

Remove the first element satisfying a predicate, or raise Not_found

val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a

Remove and return the first element satisfying a predicate, or raise Not_found

val find_map : ('a -> 'b option) -> 'a list -> 'b

Returns the first element that is mapped to Some _. Raise Not_found if there is none.

exception IndexOutOfRange
val goto : int -> 'a list -> 'a list * 'a list

goto i l splits l into two lists (l1,l2) such that (List.rev l1)++l2=l and l1 has length i. It raises IndexOutOfRange when i is negative or greater than the length of l.

val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list

split_when p l splits l into two lists (l1,a::l2) such that l1++(a::l2)=l, p a=true and p b = false for every element b of l1. if there is no such a, then it returns (l,[]) instead.

val sep_first : 'a list -> 'a * 'a list

sep_first l returns (a,l') such that l is a::l'. It raises Failure _ if the list is empty.

val sep_last : 'a list -> 'a * 'a list

sep_last l returns (a,l') such that l is l'@[a]. It raises Failure _ if the list is empty.

val drop_last : 'a list -> 'a list

Remove the last element of the list. It raises Failure _ if the list is empty. This is the second part of sep_last.

val last : 'a list -> 'a

Return the last element of the list. It raises Failure _ if the list is empty. This is the first part of sep_last.

val lastn : int -> 'a list -> 'a list

lastn n l returns the n last elements of l. It raises Failure _ if n is less than 0 or larger than the length of l

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

chop i l splits l into two lists (l1,l2) such that l1++l2=l and l1 has length i. It raises Failure _ when i is negative or greater than the length of l.

val firstn : int -> 'a list -> 'a list

firstn n l Returns the n first elements of l. It raises Failure _ if n negative or too large. This is the first part of chop.

val skipn : int -> 'a list -> 'a list

skipn n l drops the n first elements of l. It raises Failure _ if n is less than 0 or larger than the length of l. This is the second part of chop.

val skipn_at_least : int -> 'a list -> 'a list

Same as skipn but returns if n is larger than the length of the list.

val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list

drop_prefix eq l1 l returns l2 if l=l1++l2 else return l.

val insert : 'a eq -> 'a -> 'a list -> 'a list

Insert at the (first) position so that if the list is ordered wrt to the total order given as argument, the order is preserved

val share_tails : 'a eq -> 'a list -> 'a list -> 'a list * 'a list * 'a list

share_tails l1 l2 returns (l1',l2',l) such that l1 is l1'\@l and l2 is l2'\@l and l is maximal amongst all such decompositions

Association lists
val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list

Applies a function on the codomain of an association list

val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b

Like List.assoc but using the equality given as argument

val assoc_f_opt : 'a eq -> 'a -> ('a * 'b) list -> 'b option

Like List.assoc_opt but using the equality given as argument

val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list

Remove first matching element; unchanged if no such element

val mem_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> bool

Like List.mem_assoc but using the equality given as argument

val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list

Create a list of associations from a list of pairs

Operations on lists of tuples
val split : ('a * 'b) list -> 'a list * 'b list

Like OCaml's List.split but tail-recursive.

val combine : 'a list -> 'b list -> ('a * 'b) list

Like OCaml's List.combine but tail-recursive.

val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list

Like split but for triples

val split4 : ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list

Like split but for quads

val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list

Like combine but for triples

Operations on lists seen as sets, preserving uniqueness of elements
val add_set : 'a eq -> 'a -> 'a list -> 'a list

add_set x l adds x in l if it is not already there, or returns l otherwise.

val eq_set : 'a eq -> 'a list eq

Test equality up to permutation. It respects multiple occurrences and thus works also on multisets.

val subset : 'a list eq

Tell if a list is a subset of another up to permutation. It expects each element to occur only once.

val merge_set : 'a cmp -> 'a list -> 'a list -> 'a list

Merge two sorted lists and preserves the uniqueness property.

val intersect : 'a eq -> 'a list -> 'a list -> 'a list

Return the intersection of two lists, assuming and preserving uniqueness of elements

val union : 'a eq -> 'a list -> 'a list -> 'a list

Return the union of two lists, assuming and preserving uniqueness of elements

val unionq : 'a list -> 'a list -> 'a list

union specialized to physical equality

val subtract : 'a eq -> 'a list -> 'a list -> 'a list

Remove from the first list all elements from the second list.

val subtractq : 'a list -> 'a list -> 'a list

subtract specialized to physical equality

Uniqueness and duplication
val distinct : 'a list -> bool

Return true if all elements of the list are distinct.

val distinct_f : 'a cmp -> 'a list -> bool

Like distinct but using the equality given as argument

val duplicates : 'a eq -> 'a list -> 'a list

Return the list of unique elements which appear at least twice. Elements are kept in the order of their first appearance.

val uniquize_key : ('a -> 'b) -> 'a list -> 'a list

Return the list of elements without duplicates using the function to associate a comparison key to each element. This is the list unchanged if there was none.

val uniquize : 'a list -> 'a list

Return the list of elements without duplicates. This is the list unchanged if there was none.

val sort_uniquize : 'a cmp -> 'a list -> 'a list

Return a sorted version of a list without duplicates according to some comparison function.

val min : 'a cmp -> 'a list -> 'a

Return minimum element according to some comparison function.

  • raises Not_found

    on an empty list.

Cartesian product
val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list

A generic binary cartesian product: for any operator (**), cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1], and so on if there are more elements in the lists.

val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list

cartesians op init l is an n-ary cartesian product: it builds the list of all op a1 .. (op an init) .. for a1, ..., an in the product of the elements of the lists

val combinations : 'a list list -> 'a list list

combinations l returns the list of n_1 * ... * n_p tuples [a11;...;ap1];...;[a1n_1;...;apn_pd] whenever l is a list [a11;..;a1n_1];...;[ap1;apn_p]; otherwise said, it is cartesians (::) [] l

val cartesians_filter : ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list

Like cartesians op init l but keep only the tuples for which op returns Some _ on all the elements of the tuple.

module Smart : sig ... end

When returning a list of same type as the input, maximally shares the suffix of the output which is physically equal to the corresponding suffix of the input

module type MonoS = sig ... end
OCaml

Innovation. Community. Security.