代码之家 › 专栏 › 技术社区 › ice1000

当Agda/Idris无法做到时,Coq可以做什么?

idris agda coq

ice1000 · 技术社区 · 8 年前

Coq是一种证明助手,而Agda/Idris是编程语言(尽管它们可以称为证明助手)。

我在探索这些语言,我想知道Agda/Idris是否足以完成Coq所能做的一切。

那么,是否有一些[管理代码/IDE(Emacs)函数的证明/方法/其他东西]是Coq可以做的,而Agda/Idris不能做的?

1 回复 | 直到 8 年前

Thorsten Altenkirch 8 年前

Coq已经存在了一段时间,拥有一个强大的社区,拥有许多图书馆和开发项目。它还有一个战术语言和一些其他扩展,使其非常适合更大的项目。就coq核心语言而言,它通常提供的内容少于Agda。例如,很难通过模式匹配来定义函数(即使有一个扩展可以提供帮助),而且它不具有归纳-归纳类型或混合归纳和共归纳的特性。大多数coq开发不使用依赖类型(因为它们很难在coq中使用),而是使用简单(或多态类型)程序与顶部谓词的组合。

推荐文章

Mei Zhang · 定义“依赖类型”模函子

8 年前

Jason Hu · 参见Ltac中的Hintbase

8 年前

lllllllllllll · 通过两个实现对阶乘程序进行Coq验证

8 年前

MikkelBybjerg · 如何延迟lambda评估,以便替换lambda

8 年前

user9335697 · 实例化参数以评估函数定义

8 年前

Jian Wang · Coq中的背景目标、搁置目标和放弃目标是什么?

8 年前

Pablo Inostroza · 有没有可能表达一个定理,说明应用了哪些构造函数?

8 年前

jmite · Coq:在校样脚本编写期间查看校样术语

8 年前

ConfusedFormalizer · a是怎样的。vo文件的结构是否便于coqchk使用?

8 年前

Siddharth Bhat · 查看所有已安装的库以及如何在Coq中导入它们

8 年前