@@ -1,3 +1,14 @@
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`.
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`.
11+ A good example of this idiom at work is `Data.List.Views.splitRec` from `base`.
2## Tool Updates
13## Tool Updates