package coq-core

  1. Overview
  2. Docs
package coq-core
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.

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