What can Coq do while Agda/Idris can't do?

Question

Coq is a proof assistant, while Agda/Idris are programming languages (although they can be called proof assistants).

I was exploring these languages and I wonder if Agda/Idris are sufficient to do everything that Coq can do.

So, is there some [proof/way of managing code/IDE (Emacs) functions/something else] that Coq can do while Agda/Idris can't do?

Answer 1

Coq has been around for a while and has a strong community with many libraries and developments. It also has got a tactic language and some other extensions which make it very suitable for bigger projects. As far as the coq core language is concerned it often offers less than for example Agda. For example it is hard to define functions by pattern matching (even though there is an extension which helps) and it doesn't feature inductive-inductive types or mixing induction and coinduction. Most coq developments don't use dependent types (because they are difficult to use in coq) but instead use rather the combination of simply (or polymorphically typed) programs with predicates on top.