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