Module Prelude_extracted.List

List module

This module contains many safe functions for manipulating lists.

type 'a t = 'a list
val empty : 'a list
val is_empty : 'a list -> bool

Test whether a list is empty

val cons : 'a -> 'a list -> 'a list

cons x l prepends x to the beginning of l, returning a new list

val return : 'a -> 'a list

Singleton list

val hd : 'a list -> 'a

Partial function to access the head of the list. This function will fail when applied to the empty list. NOTE it is recommended to rely on pattern matching instead

val tl : 'a list -> 'a list

Partial function to access the tail of the list. This function will fail when applied to the empty list NOTE it is recommended to rely on pattern matching instead

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

List append / concatenation. append l1 l2 returns a list composed of all elements of l1, followed by all elements of l2

val append_to_nil : 'a list -> bool
val append_single : 'a -> 'a list -> 'a list -> bool
val rev : 'a list -> 'a list

Reverse a list

val length : 'a list -> Imandrax_util.Z.t

Compute the length of a list. Linear time.

val len_nonnegative : 'a list -> bool

Length of a list is non-negative. This useful theorem is installed as a forward-chaining rule.

val len_zero_is_empty : 'a list -> bool

A list has length zero iff it is empty. This is a useful rewrite rule for obtaining empty lists.

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

The length of (x @ y) is the sum of the lengths of x and y

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

Split a list of pairs into a pair of lists

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

Map a function over a list.

  • map f [] = []
  • map f [x] = [f x]
  • map f (x :: tail) = f x :: map f tail
val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> ('c list, string) result
val for_all : ('a -> bool) -> 'a list -> bool

for_all f l tests whether all elements of l satisfy the predicate f

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

exists f l tests whether there is an element of l that satisfies the predicate f

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

Fold-left, with an accumulator that makes induction more challenging

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

Fold-right, without accumulator. This is generally more friendly for induction than fold_left.

val mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
val filter : ('a -> bool) -> 'a list -> 'a list

filter f l keeps only the elements of l that satisfy f.

val filter_map : ('a -> 'b option) -> 'a list -> 'b list
val flat_map : ('a -> 'b list) -> 'a list -> 'b list
val find : ('a -> bool) -> 'a list -> 'a option

find f l returns Some x if x is the first element of l such that f x is true. Otherwise it returns None

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

mem x l returns true iff x is an element of l

val mem_assoc : 'a -> ('a * 'b) list -> bool
val nth : Imandrax_util.Z.t -> 'a list -> 'a option
val assoc : 'a -> ('a * 'b) list -> 'b option
val bounded_recons : int -> 'a list -> 'a list

Like take n l, but measured subset is n instead of l.

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

take n l returns a list composed of the first (at most) n elements of l. If length l <= n then it returns l

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

drop n l returns l where the first (at most) n elements have been removed. If length l <= n then it returns []

val range : int -> int -> int list

Integer range. i -- j is the list [i; i+1; i+2; …; j-1]. Returns the empty list if i >= j.

val (--) : int -> int -> int list
val insert_sorted : leq:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list

Insert x in l, keeping l sorted.

val sort : leq:('a -> 'a -> bool) -> 'a list -> 'a list

Basic sorting function

val is_sorted : leq:('a -> 'a -> bool) -> 'a list -> bool

Check whether a list is sorted, using the leq less-than-or-equal predicate

val monoid_product : 'a list -> 'b list -> ('a * 'b) list
val (>|=) : 'a list -> ('a -> 'b) -> 'b list
val (>>=) : 'a list -> ('a -> 'b list) -> 'b list
val let+ : 'a list -> ('a -> 'b) -> 'b list
val and+ : 'a list -> 'b list -> ('a * 'b) list
val let* : 'a list -> ('a -> 'b list) -> 'b list
val and* : 'a list -> 'b list -> ('a * 'b) list