Res.DefStrat
Default strategy for resizable datastructures
type t
is a triple (waste, shrink_trig, min_size)
, where waste
(default: 1.5) indicates how much the array should grow in excess when reallocation is triggered, shrink_trig
(default: 0.5) at which percentage of excess elements it should be shrunk and min_size
(default: 16 elements) is the minimum size of the resizable array.