3 ms·
One thing I love about Agda is that it translates to Idris (which is much more friendly to a regular programmer) almost mechanically. Once I needed to write a
by lightgreen 7y ago
One thing I love about Agda is that it translates to Idris (which is much more friendly to a regular programmer) almost mechanically.
Once I needed to write a proof of permutation transitivity in Idris. I’m not smart enough to write it myself, but I found a proof in Agda and translated it to Idris in 20 minutes. https://github.com/stepancheg/idris-sort/blob/master/PermHard.idr https://github.com/stepancheg/idris-sort/blob/master/PermHar...
- riedel 7y agoI was delighted to see that both idris and agda have JavaScript backends. Is there actually any productive use for that? Particularly looking at all the excitement around Reason .
- gergoerdi 7y agoHere's a toy example: a single-page web app written in Idris. https://github.com/gergoerdi/icfp-bingo-2017-idris https://github.com/gergoerdi/icfp-bingo-2017-idris