Module CCList.RefSource

push rlist e adds an element e at the head of rlist.

pop rlist removes and returns Some e (the first element of rlist) or None if the rlist is empty

pop_exn rlist removes and returns the first element of rlist. Unsafe version of pop.

• raises Failure

  if the list is empty.

create () creates a new empty reference list.

clear rlist removes all elements of rlist.

lift f rlist applies a list function f to the content of rlist.

push_list rlist l adds elements of the list l at the beginning of the list ref rlist. Elements at the end of the list l will be at the beginning of the list ref rlist.