What can Kok do until Agda / Idris can do this?

Question

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

I studied these languages ​​and I wonder if Agda / Idris is enough to do everything Kok can do.

So, is there a [proof / way of managing functions / IDE (Emacs) / something else] that Coq can do when Agda / Idris cannot do it?

Answer 1

Coq has existed for some time and has a strong community with many libraries and developments. It also has a tactical language and some other extensions that make it very suitable for large projects. As for the main coq language, it often offers less than, for example, Agda. For example, it is difficult to define functions using pattern matching (although there is an extension that helps), and it does not have inductive types or a mixture of induction and coinduction. Most coq designs do not use dependent types (because they are difficult to use in coq), but rather use a combination of simple (or polymorphically typed) programs with predicates at the top.