Module miri::range_map

source ·
Expand description

Implements a map from integer indices to data. Rather than storing data for every index, internally, this maps entire ranges to the data. To this end, the APIs all work on ranges, not on individual integers. Ranges are split as necessary (e.g., when [0,5) is first associated with X, and then [1,2) is mutated). Users must not depend on whether a range is coalesced or not, even though this is observable via the iteration APIs.