Module Imandra_prelude.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 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 -> Z.t

Compute the length of a list. Linear time.

val len_nonnegative : 'a list -> bool
val len_zero_is_empty : 'a list -> bool
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 ) -> base:'b -> 'a list -> 'b

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

val mapi_with : base:Z.t -> ( Z.t -> 'a -> 'b ) -> 'a list -> 'b list
val mapi : ( Z.t -> '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 : Z.t -> 'a list -> 'a option
val assoc : 'a -> ('a * 'b) list -> 'b option
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 (--) : 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 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 small-or-equal-than predicatet

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