idris-lang/Idris-dev — pull request #1662 by Melvar (2014-10-18 21:32:49+00:00)
Title: Eliminate with_val by generalizing value

To the best of my understanding, this should work perfectly, but testing with some more complex existing code would be good.