1回答
在Agda中调用函数
、、、
我有这段代码，它基本上是一个hello world，有一个加法函数，它编译并运行并输出'Hello，world 5!'open import Common.IO
zero : ℕ我是Agda的新手，网上也没有太多
浏览 14提问于2019-03-26得票数 2
回答已采纳
1回答
我在agda-mode中使用Emacs，并编写了以下函数：pow m n = pow' 1 m n pow' acc m (succ n) = pow' (m * acc) m n
Nat、succ和*被定义为与Agda在计算(pow 2 100000)时，会得到堆栈溢出错误。但是，考虑到递归调用是尾<em
浏览 1提问于2013-09-21得票数 2
回答已采纳
1回答
考虑以下(无效) Agda代码 data Example : Example ex → Set where ex : Example ex'
ex' = ex 这一切都被编译了，Agda正确地知道ex : Example ex 但是，尝试使用模式匹配来定义
浏览 21提问于2019-12-11得票数 6
回答已采纳
1回答
原因是Cubical Agda不完全支持索引归纳类型：https://github.com/agda/cubical/pull/104#discussion_r268476220 一个相关的问题指出，模式匹配不适用于归纳家族，因为还没有在归纳家族上定义hcomp和transp：https://github.com/agda/cubical/pull/57#issuecomment-461174095 我定
浏览 15提问于2020-01-28得票数 6
回答已采纳
1回答
类似Agda的Coq/编程？
、、、、
与Agda不同，Coq倾向于将证明与函数分开。Coq给出的策略非常适合编写证据，但我想知道是否有一种方法可以复制Agda模式的功能。
相当于Agda模式下的C- C -r (reify)，在这里您用函数填充?当我在一个函数中执行match时，让Coq自动写出可能的分支(比如
浏览 6提问于2017-01-24得票数 10
回答已采纳
我试图从Sipser的计算理论中实现第一个示例，并得到一个无法识别的黄色高亮显示。一般情况下，如何在Agda中调试这些约束错误，特别是在我的示例中？首先，有没有什么成功的方法可以避免它们呢?/toy.agda:60,18-23 ]
_r3_62 : rule Sipser1 [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/
浏览 25提问于2020-09-20得票数 2
回答已采纳
我已经安装并能够通过emacs编辑器在我的Ubuntu系统上使用Agda，到目前为止一切似乎都很好。apt-get install agda-stdlib代数函数IO.agda关系Algebra.agdaFunction.agda IO.agdai Size.agda Algebra.agdai Functi
浏览 2提问于2020-04-29得票数 4
回答已采纳
1回答
我试图在agda中定义二进制数，但是agda看不到⟦_⇑⟧正在终止。我真的不想打破可访问性的关系。如何向agda显示n变小了？
浏览 1提问于2019-11-11得票数 1
回答已采纳
1回答
我想知道是否有人在Agda中找到了解决以下问题的方法。我想传递一个自然数n作为参数给一个Agda模块。在这个模块中，我构造了一个接受Fin n类型参数的函数。当模式与该函数的参数匹配时，我会遇到这样的问题：n可能是zero，因此Fin n类型将为空。Agda将不接受Fin的zero和suc _构造函数。奇怪的是，当您在函数本身中引入原始自然数时，Agda似乎没有这个问题，而且该函数编译得很好。pat
浏览 2提问于2016-04-21得票数 2
回答已采纳
我编写了一个函数来获取除了std中的List的最后一个元素之外的所有内容：allButLast (x ∷ []) = []为了证明起见，我想用∷ʳ重写这个函数∷ʳ (infixl operator, level 5) [_∷ʳ_ (/Users/fss/
浏览 7提问于2020-11-28得票数 0
回答已采纳
2回答
当我在Agda中玩弄证明验证时，我意识到我对一些类型明确地使用了归纳原理，而在其他情况下使用了模式匹配。我终于在维基百科上找到了一些关于模式匹配和归纳原则的文章：“在Agda中，依赖类型的模式匹配是语言的原语，核心语言没有模式匹配转换成的归纳/递归原则。”那么，Agda中的类型理论归纳和递归原则(在类型上定义函数)是否因为Agdas模式匹配而完全多余？像这样的东西()只会有教学价值。
浏览 20提问于2015-06-02得票数 5
我刚开始学习Agda阅读。在第一章中，有一个乘法的定义，其中一种情况是(suc m) * n = n + (m * n)。Operators used in the grammar: + (infix operator, level 20) [_+_
浏览 18提问于2020-05-10得票数 2
我有一个将自然数映射到其对应的Agda宇宙级别的函数。lzeroSetn l = Set (level l) 我在定义归纳数据类型时以如下方式使用此函数Lift : {l' : Nat} -> {l' <= l} -> U l' -> U l 在这里，Agda抱怨Set (level l')不
浏览 15提问于2020-07-06得票数 4
回答已采纳
我需要帮助使agda模式在我的emacs系统上工作。本质上，语法突出显示只发生在我保存之后，而不像其他标准模式那样是实时的。我做了基础教程。我在我的系统上运行Manjaro，所以我使用pacman来安装agda (2.6.0.1)和(1.2-1)。"agda-mode locate")))
到我.emacs.d文件中的.emacs.d。然而，当我启动emacs时，我尝试使用我在网上找到的一些文件来学习agda ( )。但是，只有在保
浏览 4提问于2020-03-02得票数 0
回答已采纳
1回答
我想知道是否有一种系统的方法来解释Coq定义为agda程序。我正在翻译部分编程基础，无法让tUpdate函数在下面工作。为什么这个失败。对coq代码进行注释。编辑：
我意识到更新应该返回一张地图，但我很困惑，因为它似乎可以推断出这一点，而agda不能？对于后一个问题，我仍然欢迎一个更笼统的答案。
浏览 2提问于2020-04-10得票数 1
回答已采纳
1回答
由于Nat的_+_-Operation通常在第一个参数中以递归方式定义，因此类型检查器知道该i + 0 == i显然不是一件微不足道的事情。然而，当我在固定大小的向量上编写函数时，我经常遇到这个问题。一个例子:如何定义Agda函数将第一个n值放在向量的末尾？因为在Haskell中一个简单解决方案应该是swap n
浏览 5提问于2012-10-18得票数 18
回答已采纳
如果我有一个函数domain，它返回函数类型的域，我可以将这个证明写成但我认为写这样的函数是不可能的。
有办法这样做吗？
浏览 3提问于2014-01-25得票数 1
回答已采纳
在使用Agda (agda --compile hello-world.agda)编译时，报告了以下错误： $HOME/hello-world.agda:5,8-11
报告的位置(5,8-11)对应于令牌run。我没有在Agda和Agda-stdlib问题中找到任何相关信息，也没有在这样或其他网站上找到任何相关信息。文件是过期了，还是我犯了什么错误？注意
浏览 6提问于2021-03-06得票数 1
回答已采纳
云服务器
ICP备案
腾讯会议
云直播
对象存储
腾讯云开发者
