未解决的metas将在Agda hello-world中运行
未解决的metas将在Agda hello-world中运行
提问于 2021-03-06 11:42:38
我试图用你好-世界和Agda stdlib 1.5编译这个示例。以下是代码：
module hello-world where
open import IO
main = run (putStrLn "Hello, World!")在使用Agda (agda --compile hello-world.agda)编译时，报告了以下错误：
Unsolved metas at the following locations:
$HOME/hello-world.agda:5,8-11报告的位置(5,8-11)对应于令牌run。
我没有在Agda和Agda-stdlib问题中找到任何相关信息，也没有在这样或其他网站上找到任何相关信息。文件是过期了，还是我犯了什么错误？
注意：
- Agda编译器安装在带有解析器
stack install Agda的lts-17.5中。 - 我还尝试从GitHub源代码(分支
release-2.6.1.3)手动编译。 - 在
$HOME/.agda/libraries中，我有：$HOME/agda/standard.agda-lib - 在
$HOME/.agda/defaults中我有:标准库
回答 1
Stack Overflow用户
回答已采纳
发布于 2021-03-06 13:00:55
这就是https://github.com/agda/agda/issues/4250#issuecomment-771806949评论中描述的问题。当前的解决方法是向run添加一个隐式参数，如下所示：
module hello-world where
open import IO
open import Level
main = run {0ℓ} (putStrLn "Hello, World!")这个问题将在即将发布的Agda 2.6.2和标准库的下一个版本中得到修正。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/66505255
复制相关文章
相似问题
腾讯云开发者
