package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
doc/coq-core.lib/Util/List/index.html
Module Util.ListSource
include module type of List
An alias for the type of lists.
Return the length (number of elements) of the given list.
Compare the lengths of two lists. compare_lengths l1 l2 is equivalent to compare (length l1) (length l2), except that the computation stops after reaching the end of the shortest list.
Compare the length of a list to an integer. compare_length_with l len is equivalent to compare (length l) len, except that the computation stops after at most len iterations on the list.
cons x xs is x :: xs
Return the first element of the given list.
Return the given list without its first element.
Return the n-th element of the given list. The first element (head of the list) is at position 0.
Return the n-th element of the given list. The first element (head of the list) is at position 0. Return None if the list is too short.
List reversal.
rev_append l1 l2 reverses l1 and concatenates it with l2. This is equivalent to (rev l1) @ l2.
Comparison
Iterators
iter f [a1; ...; an] applies function f in turn to [a1; ...; an]. It is equivalent to f a1; f a2; ...; f an.
Same as iter, but the function is applied to the index of the element as first argument (counting from 0), and the element itself as second argument.
Same as map, but the function is applied to the index of the element as first argument (counting from 0), and the element itself as second argument.
filter_map f l applies f to every element of l, filters out the None elements and returns the list of the arguments of the Some elements.
fold_left f init [b1; ...; bn] is f (... (f (f init b1) b2) ...) bn.
fold_right f [a1; ...; an] init is f a1 (f a2 (... (f an init) ...)). Not tail-recursive.
Iterators on two lists
iter2 f [a1; ...; an] [b1; ...; bn] calls in turn f a1 b1; ...; f an bn.
fold_left2 f init [a1; ...; an] [b1; ...; bn] is f (... (f (f init a1 b1) a2 b2) ...) an bn.
fold_right2 f [a1; ...; an] [b1; ...; bn] init is f a1 b1 (f a2 b2 (... (f an bn init) ...)).
List scanning
for_all f [a1; ...; an] checks if all elements of the list satisfy the predicate f. That is, it returns (f a1) && (f a2) && ... && (f an) for a non-empty list and true if the list is empty.
exists f [a1; ...; an] checks if at least one element of the list satisfies the predicate f. That is, it returns (f a1) || (f a2) || ... || (f an) for a non-empty list and false if the list is empty.
Same as for_all, but for a two-argument predicate.
Same as exists, but for a two-argument predicate.
mem a set is true if and only if a is equal to an element of set.
Same as mem, but uses physical equality instead of structural equality to compare list elements.
List searching
find f l returns the first element of the list l that satisfies the predicate f.
find f l returns the first element of the list l that satisfies the predicate f. Returns None if there is no value that satisfies f in the list l.
find_index f xs returns Some i, where i is the index of the first element of the list xs that satisfies f x, if there is such an element.
It returns None if there is no such element.
Same as find_map, but the predicate is applied to the index of the element as first argument (counting from 0), and the element itself as second argument.
List manipulation
take n l returns the prefix of l of length n, or a copy of l if n > length l.
n must be nonnegative.
drop n l returns the suffix of l after n elements, or [] if n > length l.
n must be nonnegative.
take_while p l is the longest (possibly empty) prefix of l containing only elements that satisfy p.
drop_while p l is the longest (possibly empty) suffix of l starting at the first element that does not satisfy p.
partition f l returns a pair of lists (l1, l2), where l1 is the list of all the elements of l that satisfy the predicate f, and l2 is the list of all the elements of l that do not satisfy f. The order of the elements in the input list is preserved.
partition_map f l returns a pair of lists (l1, l2) such that, for each element x of the input list l:
- if
f xisLeft y1, theny1is inl1, and - if
f xisRight y2, theny2is inl2.
The output elements are included in l1 and l2 in the same relative order as the corresponding input elements in l.
In particular, partition_map (fun x -> if f x then Left x else Right x) l is equivalent to partition f l.
Association lists
assoc a l returns the value associated with key a in the list of pairs l. That is, assoc a [ ...; (a,b); ...] = b if (a,b) is the leftmost binding of a in list l.
assoc_opt a l returns the value associated with key a in the list of pairs l. That is, assoc_opt a [ ...; (a,b); ...] = Some b if (a,b) is the leftmost binding of a in list l. Returns None if there is no value associated with a in the list l.
Same as assoc, but uses physical equality instead of structural equality to compare keys.
Same as assoc_opt, but uses physical equality instead of structural equality to compare keys.
Same as assoc, but simply return true if a binding exists, and false if no bindings exist for the given key.
Same as mem_assoc, but uses physical equality instead of structural equality to compare keys.
remove_assoc a l returns the list of pairs l without the first pair with key a, if any. Not tail-recursive.
Same as remove_assoc, but uses physical equality instead of structural equality to compare keys. Not tail-recursive.
Lists of pairs
Sorting
Sort a list in increasing order according to a comparison function. The comparison function must return 0 if its arguments compare as equal, a positive integer if the first is greater, and a negative integer if the first is smaller (see Array.sort for a complete specification). For example, Stdlib.compare is a suitable comparison function. The resulting list is sorted in increasing order. sort is guaranteed to run in constant heap space (in addition to the size of the result list) and logarithmic stack space.
The current implementation uses Merge Sort. It runs in constant heap space and logarithmic stack space.
Same as sort, but the sorting algorithm is guaranteed to be stable (i.e. elements that compare equal are kept in their original order).
The current implementation uses Merge Sort. It runs in constant heap space and logarithmic stack space.
Same as sort or stable_sort, whichever is faster on typical input.
Same as sort, but also remove duplicates.
Merge two lists: Assuming that l1 and l2 are sorted according to the comparison function cmp, merge cmp l1 l2 will return a sorted list containing all the elements of l1 and l2. If several elements compare equal, the elements of l1 will be before the elements of l2. Not tail-recursive (sum of the lengths of the arguments).
Lists and Sequences
Equality, testing
Check whether a list is empty
Same as List.for_all but with an index
Same as List.for_all2 but returning false when of different length
Same as List.exists but with an index
prefix_of eq l1 l2 returns true if l1 is a prefix of l2, false otherwise. It uses eq to compare elements
A more efficient variant of for_all2eq (fun _ _ -> true)
Creating lists
interval i j creates the list [i; i + 1; ...; j], or [] when j <= i.
make n x returns a list made of n times x. Raise Invalid_argument _ if n is negative.
addn n x l adds n times x on the left of l.
init n f constructs the list f 0; ... ; f (n - 1). Raise Invalid_argument _ if n is negative
Like OCaml's List.append but tail-recursive.
Like OCaml's List.concat but tail-recursive.
Synonymous of concat
Lists as arrays
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
Like OCaml List.filter but tail-recursive and physically returns the original list if the predicate holds for all elements.
Like List.filter but with 2 arguments, raise Invalid_argument _ if the lists are not of same length.
Like List.filter but with an index starting from 0
filter_with bl l selects elements of l whose corresponding element in bl is true. Raise Invalid_argument _ if sizes differ.
Like map but keeping only non-None elements
Like map_filter but with an index starting from 0
Like List.partition but with an index starting from 0
Applying functorially
Like OCaml List.map but tail-recursive
Like OCaml List.map2 but tail-recursive
As map but ensures the left-to-right order of evaluation.
Like OCaml List.mapi but tail-recursive. Alternatively, like map but with an index
Like map2 but with an index
Like map but for 3 lists.
val map4 :
('a -> 'b -> 'c -> 'd -> 'e) ->
'a list ->
'b list ->
'c list ->
'd list ->
'e listLike map but for 4 lists.
map_of_array f a behaves as List.map f (Array.to_list a)
map_append f [x1; ...; xn] returns f x1 @ ... @ f xn.
Like map_append but for two lists; raises Invalid_argument _ if the two lists do not have the same length.
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
Count the number of elements satisfying a predicate
Finding position
index returns the 1st index of an element in a list (counting from 1).
safe_index returns the 1st index of an element in a list (counting from 1) and None otherwise.
index0 behaves as index except that it starts counting at 0.
Folding
acts like fold_left f acc s while f returns Cont acc'; it stops returning c as soon as f returns Stop c.
Like List.fold_right but with an index
Like List.fold_left but with an index
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 []
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 ->
'aFold 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)
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
Same, folding on the right
Same with two lists, folding on the left
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 listSame 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 listSame with four lists, folding on the left
Splitting
Remove the first element satisfying a predicate, or raise Not_found
Remove and return the first element satisfying a predicate, or raise Not_found
find_map f l applies f to the elements of l in order, and returns the first result of the form Some v, or None if none exist.
In stdlib since OCaml 4.10.0
Like find_map but raises Not_found instead of returning None.
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.
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.
sep_first l returns (a,l') such that l is a::l'. It raises Failure _ if the list is empty.
sep_last l returns (a,l') such that l is l'@[a]. It raises Failure _ if the list is empty.
Remove the last element of the list. It raises Failure _ if the list is empty. This is the second part of sep_last.
Return the last element of the list. It raises Failure _ if the list is empty. This is the first part of sep_last.
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
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.
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.
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.
Same as skipn but returns if n is larger than the length of the list.
drop_prefix eq l1 l returns l2 if l=l1++l2 else return l.
Insert at the (first) position so that if the list is ordered wrt to the total order given as argument, the order is preserved
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
Applies a function on the codomain of an association list
Like List.assoc but using the equality given as argument
Like List.assoc_opt but using the equality given as argument
Remove first matching element; unchanged if no such element
Like List.mem_assoc but using the equality given as argument
Create a list of associations from a list of pairs
Operations on lists of tuples
Like OCaml's List.split but tail-recursive.
Like OCaml's List.combine but tail-recursive.
Like split but for triples
Like split but for quads
Like combine but for triples
Operations on lists seen as sets, preserving uniqueness of elements
add_set x l adds x in l if it is not already there, or returns l otherwise.
Test equality up to permutation. It respects multiple occurrences and thus works also on multisets.
Tell if a list is a subset of another up to permutation. It expects each element to occur only once.
Merge two sorted lists and preserves the uniqueness property.
Return the intersection of two lists, assuming and preserving uniqueness of elements
Return the union of two lists, assuming and preserving uniqueness of elements
union specialized to physical equality
Remove from the first list all elements from the second list.
subtract specialized to physical equality
Uniqueness and duplication
Return true if all elements of the list are distinct.
Like distinct but using the equality given as argument
Return the list of unique elements which appear at least twice. Elements are kept in the order of their first appearance.
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.
Return the list of elements without duplicates. This is the list unchanged if there was none.
Return a sorted version of a list without duplicates according to some comparison function.
Return minimum element according to some comparison function.
Cartesian product
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.
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
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
Like cartesians op init l but keep only the tuples for which op returns Some _ on all the elements of the tuple.
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