Mapping

Last modified: 07 March 2024

A helper type used by map and sorted_map.