Closed
Description
We shouldn't be able to introduce bugs like I did when refactoring IO
(fixed in #1451) or the readMaybe
one discussed in agda/agda/issues/5288.
One piece of the puzzle is to have a golden test framework and have
a lot of tests involving the standard library's more "stringly typed"
functions.
A possible source of inspiration:
https://github.com/idris-lang/Idris2/blob/master/libs/test/Test/Golden.idr