@@ -9,13 +9,17 @@
99 most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)
1010
1111+ `Prelude.WellFounded` now contains an interface `Sized a` that defines a size
12− mapping from `a` to natural numbers. For example, there is an implementation
13− `Sized (List a)` where `size = length`.
12+ mapping from `a` to `Nat`. For example, there is an implementation for lists,
13+ where `size = length`.
1414
1515 The function `sizeAccessible` then proves well-foundedness of the relation
1616 `Smaller x y = LT (size x) (size y)`, which allows us to use strong
1717 induction conveniently with any type that implements `Sized`.
1818
19+ In practice, this allows us to write functions that recurse not only on
20+ direct subterms of their arguments but on any value
21+ with a (strictly) smaller `size`.
22+
1923 A good example of this idiom at work is `Data.List.Views.splitRec` from `base`.
2024
2125## Tool Updates