Page
Library
Module
Module type
Parameter
Class
Class type
Source
Containers.ListContextSourceThis module implements list contexts.
The type of the list contexts
The type for focused lists, i.e., lists with there context
forward ~step f_l moves forward (if step is greater than 0) or backward (if step is less than 0) in f_l. step defaults to 1.
right f_l moves forward (i.e., right) in the focused list. It is the same as forward f_l
left f_l moves backward (i.e., left) in the focused list. It is the same as forward ~step:(-1) f_l
zip_up f_l moves left in the focused list f_l until the context is empty and returns the list to which it is the context
fold (c, l) f acc runs f ... f (right (right (c, l))) (f (right (c, l)) (f (c, l) acc)) until no move to right is allows.
full_left f_c returns the same focused list as (empty, zip_up f_l).
forward_insert elt (z, l) returns (z, elt :: l), i.e., the list l to which elt was added, in the same context as l.
backward_insert elt (z, l) returns (push elt z, l), i.e., the list l in the context z to which elt was added.
nth_context i [a_1; …; a_i; …; a_n] returns Ok with a pair made of the focused list (z, [a_i+1 …; a_n]) and a_i such that [a_1; ….; a_n] = zip_up (z, ([a_i; a_i+1; …; a_n])) = zip_up (forward_insert a_i (z, [a_i+1 …; a_n])). Returns Error (Move_failure Right) if i is strictly greater than n.