Is there any reason to use Agda over Coq or vice versa? | Hacker News

Hacker News new | past | comments | ask | show | jobs | submit

login

kxyvr on Dec 3, 2014 | parent | context | favorite | on: Learn You an Agda

Is there any reason to use Agda over Coq or vice versa?

cies on Dec 3, 2014 [–]

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVs...

You might also want to compare to Idris (and maybe Epigram, but its no longer in development).

http://www.quora.com/How-does-Idris-compare-to-other-depende...

http://www.reddit.com/r/haskell/comments/132kg0/agda_epigram...

http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_...

http://stackoverflow.com/questions/9472488/differences-betwe...

All have pros and cons; i like that Idris can compile to JS (https://raichoo.github.io/posts/2014-01-28-improved.html)

Consider applying for YC's Spring batch! Applications are open till Feb 11.
Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact