Mapping

Last modified: 23 March 2021

A helper type used by map and sorted_map.