我需要帮助使agda模式在我的emacs系统上工作。本质上，语法突出显示只发生在我保存之后，而不像其他标准模式那样是实时的。我做了基础教程。我在我的系统上运行Manjaro，所以我使用pacman来安装agda (2.6.0.1)和(1.2-1)。然而，当我启动emacs时，我尝试使用我在网上找到的一些文件来学习agda ( )。但是，只有在保存文件时才会出现语法突出显示，而且任何新文本在保存之前都不会着色。/agd
浏览 4提问于2020-03-02得票数 0
回答已采纳
1回答
考虑以下(无效) Agda代码 data Example : Example ex → Set where ex : Example ex'
ex' = ex 这一切都被编译了，Agda，尝试使用模式匹配来定义示例之外的函数会导致编译器崩溃 test :
浏览 21提问于2019-12-11得票数 6
回答已采纳
1回答
我有一个用Agda写的'Hello World‘程序，如下面的截图所示但是当我转到Agda > Compile时，它会要求我在第二个屏幕截图中显示一个'backend‘我尝试输入'GHC‘作为我的后端，但它只显示'/usr/share/libghc-agda-dev/MAlonzo/src: getDirectoryContents:openDirStream:不存在(
浏览 1提问于2019-08-20得票数 2
我已经安装了agda-writer，因为emacs的agda模式对我不起作用(不做UTF8字符，不做语法突出显示...？？)安装agda-writer非常简单，但我找不到任何文档，而且我发现自己无法完成最基本的任务： --如何执行类型检查？(这似乎是您希望agda为您做的最基本的事情……) --如何打开语法突出显示？基本上，我唯一能做的就是尝试“编译”；当然，这会失败，因为我还没有安装haskell，但至少它会触发语法突出显示和类型检查(？) 我在莫哈
浏览 18提问于2019-05-25得票数 1
我在C:\Users\name\AppData\Roaming\agda中创建了一个文件，并插入了标准库的路径："C:\Users\name\Desktop\agda-stdlib-master\standard-library.agda-lib“，它显示我找不到它。
浏览 26提问于2019-03-01得票数 3
回答已采纳
我安装了一个Agda编译器，二进制可以从这里获得：但我以前从未使用过Emacs，我不知道从哪里开始，也不知道使用哪些命令来编译和运行我刚接触Agda，它对编译器的选择似乎很有限，而且缺乏分步教程。
浏览 0提问于2018-06-18得票数 6
在中，我发现了这个：
上面给出了Haskell类型表达式的语法。就像使用数据构造函数构建数据值一样，类型值也是从类型构造函数构建的。与数据构造函数一样，类型构造函数的名称以大写字母开头。在Agda和类似的类中，infix类型的构造函数很常见。为什么不在哈斯克尔？
浏览 6提问于2015-05-04得票数 11
回答已采纳
1回答
我试图在agda中定义二进制数，但是agda看不到⟦_⇑⟧正在终止。我真的不想打破可访问性的关系。如何向agda显示n变小了？
浏览 1提问于2019-11-11得票数 1
回答已采纳
在写证明的时候，我注意到Agda的自动验证搜索经常找不到我认为很明显的解决方案。不幸的是，给出了一个很小的例子，说明了这个问题似乎很难解决，所以我试着描述最常见的模式。我忘了将-m添加到洞中，以使Agda查看模块范围。我能把那个标志设为缺省值吗？那会有什么坏处呢？
查看目标时，甚至不会显示let或wh
浏览 1提问于2014-02-26得票数 50
下面我得到了关于假设的身份函数apfId的黄色高亮显示。我不明白，_≡_ {A}不是有A → A → Set类型吗？有没有什么简单的方法来检查Agda中表达式的类型，比如:t在ghci中？———— Error —————————————————————————————————————————————————
/home/wmacmil/agda2020/agda/MLTT/Id.agda
浏览 27提问于2020-05-27得票数 1
1回答
然而，当我在固定大小的向量上编写函数时，我经常遇到这个问题。一个例子:如何定义Agda函数将第一个n值放在向量的末尾？因为在Haskell中一个简单解决方案应该是swap n (x:xs) = swap (n-1) (xs ++ [x])sw
浏览 5提问于2012-10-18得票数 18
回答已采纳
如何在emacs中使用TeX描述(如\beta、\alpha、\lambda等)输入希腊符号？
浏览 3提问于2011-06-08得票数 29
1回答
我已经使用Agda 9个月了。这是我第一次发现自己想要“运行”(作为顶级可执行文件)--一个打印字符串的Agda程序。叫我老派。我可以编写一个计算字符串的程序，并获得Agda来显示交互模式(或Emacs)中字符串的值。但是字符串很长，并嵌入了新行。我想把它打印出来。相比之下，在GHCi中我可以这样做：hello, world!.Data.List.List.∷ .Data.List.List.[]))
那么，我
浏览 1提问于2014-09-25得票数 6
回答已采纳
在立体Agda中，我如何证明两件事是不平等的？BUILTIN NATURAL ℕ #-}
pos : ℕ → ℤ congZero : pos 0 ≡ neg 0oddThing2 : pos 0 ≡ congZero i1我发现了一个相当难看的证据我不能再对succ a ≡ 0的证明进行模式匹配了；<em
浏览 6提问于2020-04-26得票数 4
回答已采纳
我正在尝试设置一个好的Agda环境，但一个很大的障碍是在我的Emacs设置中Unicode符号的可读性。对于频繁阅读大量Unicode的Agda源代码来说，这是一个巨大的可读性问题。
浏览 2提问于2012-01-09得票数 8
回答已采纳
1回答
在索引不明确等于i，e的情况下，必须使用引理来显示类型匹配。的问题是：，但我想知道，这样的函数是否已经在agda-stdlib中了？对于Agda来说，是否有类似于hoogle的东西，或者类似于SearchAbout的东西？
浏览 0提问于2015-01-05得票数 1
回答已采纳
我试图从Sipser的计算理论中实现第一个示例，并得到一个无法识别的黄色高亮显示。一般情况下，如何在Agda中调试这些约束错误，特别是在我的示例中？首先，有没有什么成功的方法可以避免它们呢?/toy.agda:60,18-23 ]
_r3_62 : rule Sipser1 [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_file
浏览 25提问于2020-09-20得票数 2
回答已采纳
在agda文档中，我读到，当“除了目标之外的一些元变量无法被解决时，代码将被突出显示为黄色”。stupid = refl
但是，如果我使用一个产品作为依赖产品的特例，我会得到stupid''''的黄色高亮显示对于调试agda中的黄色高亮显示错误有什么一般性的建议吗？
浏览 1提问于2020-05-18得票数 3
回答已采纳
2回答
从属对的教会编码
、、、
但是，最后一个定义失败，并显示错误消息：X : Setxy : dprod X Yy : Y x
The term "y" has
浏览 7提问于2019-03-17得票数 1
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
云直播活动推荐
腾讯云开发者
