14.2.38  Random_Access_List

The standard library Random_Access_List api defines lists which support efficient random access as well as traditional list-style access and operations.

The Random_Access_List api is implemented by the binary_random_access_list package.

The Random_Access_List api source code is in src/lib/src/random-access-list.api.

The above information is manually maintained and may contain errors.

api {    Random_Access_List X;
    empty : Random_Access_List(X );
    length : Random_Access_List(X ) -> Int;
    null : Random_Access_List(X ) -> Bool;
    cons : (X , Random_Access_List(X )) -> Random_Access_List(X );
    head : Random_Access_List(X ) -> X;
    tail : Random_Access_List(X ) -> Random_Access_List(X );
    get : (Random_Access_List(X ) , Int) -> X;
    set : (Random_Access_List(X ) , Int , X)
          -> Random_Access_List(X );
    from_list : List(X ) -> Random_Access_List(X );
    to_list : Random_Access_List(X ) -> List(X );
    map : (X -> Y)
          -> Random_Access_List(X ) -> Random_Access_List(Y );
    apply : (X -> Void) -> Random_Access_List(X ) -> Void;
    fold_left : ((X , Y) -> Y) -> Y -> Random_Access_List(X ) -> Y;
    fold_right : ((X , Y) -> Y) -> Y -> Random_Access_List(X ) -> Y;
};