@@ -1,3 +1,14 @@
1+## Library Updates
2+
3++ `Prelude.WellFounded` now contains an interface `Sized a` that defines a size
4+ mapping from `a` to natural numbers. For example, there is an implementation
5+ `Sized (List a)` where `size = length`.
6+
7+ The function `sizeAccessible` then proves well-foundedness of the relation
8+ `Smaller x y = LT (size x) (size y)`, which allows us to use strong
9+ induction conveniently with any type that implements `Sized`.
10+
11+ A good example of this idiom at work is `Data.List.Views.splitRec` from `base`.
112
213## Tool Updates
314