个人中心
文章发布
退出
作者热门文章
- html - 出于某种原因，IE8 对我的 Sass 文件中继承的 html5 CSS 不友好？
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景？
25
4
Coq是证明助手，而Agda/Idris是编程语言(尽管它们可以称为证明助手)。
我正在探索这些语言，我想知道Agda/Idris是否足以完成Coq可以做的所有事情。
那么，Coq可以执行Agda/Idris不能执行的某些[证明/管理代码/IDE(Emacs)函数的方式/其他事情]吗？
最佳答案
Coq已经存在了一段时间，并且拥有许多图书馆和开发项目的强大社区。它还具有一种战术语言和一些其他扩展，使其非常适合大型项目。
就Coq核心语言而言，它所提供的功能通常少于Agda。例如，很难通过模式匹配来定义函数(即使有扩展名也可以帮助它)，并且它不具有感应-感应类型或混合感应和共感应的功能。大多数coq开发都不使用依赖类型(因为它们很难在coq中使用)，而是使用简单(或多态类型)程序与谓词在顶部的组合。
关于coq - Coq可以做什么，而Agda/Idris不能做什么？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/47842309/
25
4
0
我有一个关于 JavaScript 语法的问题。实际上，我在自学 MEAN 堆栈教程时想出了编码(https://thinkster.io/mean-stack-tutorial#adding-aut
在我的书中它使用了这样的东西: for($ARGV[0]) { Expression && do { print "..."; last; }; ... } for 循环不完整吗？另外，do 的意义何
我已经编写了读取开关状态的代码，如果按 3 次 # 则退出。 void allkeypadTest(void) { static uint8_t modeKeyCount=0; do
因此，对于上周我必须做的作业，我必须使用 4 个 do-while 循环和 if 语句在 Java 中制作一个猜谜游戏。我无法成功完成它，类(class)已经继续，没有为我提供任何帮助。如果有人可以查
int i=1,j=0,n=10,k; do{ j+=i; i<<1; printf("%d\n",i); // printf("%d\n",12<<1); }while
此代码用于基本杂货计算器的按钮。当我按下按钮时，一个输入对话框会显示您输入商品价格的位置。我遇到的问题是我无法弄清楚如何获得 do ... while 循环以使输入对话框在输入后弹出。 我希望它始终恢
当我在循环中修改字符串或另一个变量时，它的条件是否每次都重新计算？或者在循环开始前一次 std::string a("aa"); do { a = "aaaa"; } while(a.size<10)
我刚刚写了这个，但我找不到问题。我使用代码块并编写了这个问题 error: expected 'while' before '{' token === Build finished: 1 errors
do { printf("Enter number (0-6): ", ""); scanf("%d", &Num); }while(Num >= 0 && Num 表示“超过”，<表
我有一个包含 10 个项目的 vector (为简单起见，所有项目都属于同一类，称其为“a”)。我想要做的是检查“A”不是 a) 隐藏墙壁或 b) 隐藏另一个“A”。我有一个碰撞函数可以做到这一点。
嗨，这是我的第二个问题。我有下表 |-----|-------|------|------| |._id.|..INFO.|.DONE.|.LAST.| |..1..|...A...|...N..|.
这个问题在这里已经有了答案: 关闭 12 年前。 Possible Duplicates: Why are there sometimes meaningless do/while and if/e
来自 wikibook在 F# 上有一小部分它说: What does let! do?# let! runs an async object on its own thread, then it i
我在 Real World Haskell 书中遇到了以下函数: namesMatching pat | not (isPattern pat) = do exists do
我有一个类似于下面的用例，我创建了多个图并使用 gridExtra 将它们排列到一些页面布局中，最后使用 ggsave 将其保存为 PDF : p1 % mutate(label2
当我使用具有 for 循环的嵌套 let 语句时，如果没有 (do (html5 ..))，我将无法运行内部 [:tr]。 (defpartial column-settings-layout [&
执行 vagrant up 时出现此错误: anr@anr-Lenovo-G505s ~ $ vagrant up Bringing machine 'default' up with 'virtua
# ################################################# # Subroutine to add data to the table Blas
我想创建一个检查特定日期格式的读取主机。此外，目标是检查用户输入是否正确，如果不正确，则提示应再次弹出。 当我刚接触编程时，发现了这段代码，这似乎很合适。我仍然在努力“直到” do {
我关注这个tutorial在谷歌云机器学习引擎上进行培训。我一步一步地跟着它，但是在将 ml 作业提交到云时我遇到了错误。我运行了这个命令。 sam@sam-VirtualBox:~/models/r
我是一名优秀的程序员,十分优秀！