Indexer
Indexer implements ordered collection of items with random access. It is suitable for building fast access operations in GUI tree and list widgets.
module type Elt = sig ... end
module Make (E : Elt) : sig ... end
Frama-C