Coq是证明助手，而Agda / Idris是编程语言（尽管它们可以称为证明助理）。
我正在探索这些语言，我想知道Agda / Idris是否足以完成Coq可以做的所有事情。
那么，是否有一些[证明/管理代码/ IDE（Emacs）功能/其他东西的方式] Coq可以做到而Agda / Idris无法做到？
Coq已经存在了一段时间，并且拥有一个拥有许多图书馆和开发项目的强大社区。它还有一种策略语言和一些其他扩展，使其非常适合更大的项目。就coq核心语言而言，它通常提供的不仅仅是例如Agda。例如，很难通过模式匹配来定义函数（即使有一个有帮助的扩展），并且它没有感应诱导类型或混合感应和共同诱导。大多数coq开发不使用依赖类型（因为它们难以在coq中使用），而是使用简单（或多态类型）程序与谓词的组合。