The standard library Tagged_Numbered_List api defines access to datastructures which support efficient insertion, deletion and access to items by ordinal number and also by abstract tag. The motivating example is the emacs text buffer, which supports both insertion or deletion of the n-th line and also insertion or deletion at the spot marked by a tag. The intention is to develop a simple, purely-applicative analogue of the emacs text buffer.
The Tagged_Numbered_List api is implemented by the tagged_numbered_list package from src/lib/src/tagged-numbered-list.pkg which is a proxy for the red_black_tagged_numbered_list package from src/lib/src/red-black-tagged-numbered-list.pkg.
The Tagged_Numbered_List api source code is in src/lib/src/tagged-numbered-list.api.
See also: Numbered_List.
See also: Numbered_Set.
The above information is manually maintained and may contain errors.
api {
Tagged_Numbered_List X;
Tag X;
is_empty : Tagged_Numbered_List(X ) -> Bool;
empty : Tagged_Numbered_List(X );
set : (Tagged_Numbered_List(X ) , Int , X) -> (Tagged_Numbered_List(X ) , Tag(X ));
set' : (((Int , X)) , Tagged_Numbered_List(X )) -> (Tagged_Numbered_List(X ) , Tag(X ));
$ : (Tagged_Numbered_List(X ) , ((Int , X))) -> Tagged_Numbered_List(X );
find : (Tagged_Numbered_List(X ) , Int) -> Null_Or(X );
sub : (Tagged_Numbered_List(X ) , Int) -> X;
_[] : (Tagged_Numbered_List(X ) , Int) -> X;
vals_count : Tagged_Numbered_List(X ) -> Int;
all_invariants_hold : Tagged_Numbered_List(X ) -> Bool;
debug_print : (Tagged_Numbered_List(X ) , (X -> Void)) -> Int;};