@edwinbrady https://github.com/edwinb/Idris2/blob/2938e864/libs/base/Control/App.idr#L237 …
This reification of interfaces as data in constraint position seems really compelling. Is there a name for this feature? Idris1 did not let us do this, right?
Replying to @alrunner4
Idris 2 has unified auto implicits and interface solving - they use the same mechanism now, and interfaces are (literally) just sugar for auto impicits. Probably should have done that all along, but I didn't think of it...
4:51 AM - 29 Mar 2020
0 replies
0 retweets
4 likes
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.