The type of the dependency manager

The type of the elements which the manager stores the dependencies between

The empty manager

add elt1 elt2 m returns a manager similar to m except that the dependency of elt1 on elt2 (elt1 depends on elt2) has been added

dependencies elt m returns an ordered list of the elements that are dependant from elt according to the manager m. This list is such that if i_k and i_j belong to the list and k<j then there is no dependency on i_j for i_k.

merge m1 m2 returns a new dependency manager that take into accounts all the dependencies in m1 and in m2. If some element has dependencies in m1 and in m2 then all the dependencies remain

roots m returns the list of elements that depend on no other element