Module Gospelstdlib.List

Gospel declaration:
    type 'a t = 'a list 

An alias for 'a list.

Gospel declaration:
    function length (l: 'a t) : integer 

length l is the number of elements of l.

Gospel declaration:
    function hd (l: 'a t) : 'a 

When l contains one or more elements, hd s is the first element of l.

Gospel declaration:
    function tl (l: 'a t) : 'a t 

When l contains one or more elements, tl l is the list of the elements of l, starting at position 2.

Gospel declaration:
    function nth (l: 'a t) (i: integer) : 'a 

nth l i is the ith element of l.

Gospel declaration:
    function nth_opt (l: 'a t) (i: integer) : 'a option 

nth l i is the ith element of l if i is within the bounds of l, and None otherwise.

Gospel declaration:
    function rev (l: 'a t) : 'a t 

rev l contains the same elements as l in a reverse order.

Gospel declaration:
    function init (n: integer) (f: integer -> 'a) : 'a t 

init n f is a list of length n, with element number i initialized with f i.

Gospel declaration:
    function map (f: 'a -> 'b) (l: 'a t) : 'b t 

map f l applies function f to all the elements of l, and builds a list with the results returned by f

Gospel declaration:
    function mapi (f: integer -> 'a -> 'b) (l: 'a t) : 'b t 

Same as map, but the function is applied to the index of the element as first argument, and the element itself as second argument.

Gospel declaration:
    function fold_left (f: 'a -> 'b -> 'a) (init: 'a) (l: 'b t) : 'a 

fold_left f init t is f (... (f (f init a[0]) a[1]) ...) a[n-1], where n is the length of t.

Gospel declaration:
    function fold_right (f: 'b -> 'a -> 'a) (l: 'b t) (init: 'a) : 'a 

fold_right f t init is f a[0] (f a[1] ( ... (f a[n-1] init) ...)), where n is the length of t.

Gospel declaration:
    function map2 (f: 'a -> 'b -> 'c) (l: 'a t) (l': 'b t) : 'c t 

map2 f l l' applies function f to all the elements of l and l', and builds a list with the results returned by f.

Gospel declaration:
    predicate for_all (f: 'a -> bool) (l: 'a t) 

for_all f l holds iff all elements of l satisfy the predicate f.

Gospel declaration:
    predicate _exists (f: 'a -> bool) (l: 'a t) 

_exists f l holds iff at least one element of l satisfies f.

Gospel declaration:
    predicate for_all2 (f: 'a -> 'b -> bool) (l: 'a t) (l': 'b t) 

Same as for_all, but for a two-argument predicate.

Gospel declaration:
    predicate _exists2 (f: 'a -> 'b -> bool) (l: 'a t) (l': 'b t) 

Same as _exists, but for a two-argument predicate.

Gospel declaration:
    predicate mem (x: 'a) (l: 'a t) 

mem x l holds iff x is equal to an element of l

Gospel declaration:
    function to_seq (s: 'a t) : 'a Sequence.t 
    coercion 

Gospel declaration:
    function of_seq (s: 'a Sequence.t) : 'a t