如何解决在 Agda hello-world 中运行的未解析元数据
我尝试使用 hello-world 和 Agda 2.6.1.3 编译 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 问题中找到任何相关信息,也没有在 SO 或其他网站上找到任何相关信息。文档是否过时,或者我是否犯了任何错误?
注意:
- Agda 编译器与带有解析器
stack install Agda
的lts-17.5
一起安装。 - 我还尝试从 GitHub 源(分支
release-2.6.1.3
)手动编译。 - 在
$HOME/.agda/libraries
我有:$HOME/agda-stdlib/standard-library.agda-lib
- 在
$HOME/.agda/defaults
我有:standard-library
解决方法
这是在 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 和下一版本的标准库中修复。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。