Open xekoukou opened 5 years ago
https://github.com/agda/agda/issues/3805
For example, your mergesort implementation does not work anymore. https://twitter.com/ulfnorell/status/727543430335873028
Fixing in the no-more-with-inliner branch, but blocked on agda/agda#3805/agda/agda#3870.
https://github.com/agda/agda/issues/3805