标签: agda-stdlib

我尝试使用Agda 2.6.1.3和Agda stdlib 1.5编译hello-world示例。下面是代码：

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) 对应于 token run。

我在 Agda 和 Agda-stdlib Issues 中都没有找到任何相关信息，在 SO 或其他网站上也没有找到任何相关信息。文档是否已过时，或者我是否犯了任何错误？

笔记：

• Agda 编译器是通过stack install Agda解析器安装的lts-17.5。
• 我还尝试从 GitHub 源（分支）手动编译release-2.6.1.3。
• 在$HOME/.agda/libraries我有：

  $HOME/agda-stdlib/standard-library.agda-lib
  

  Run Code Online (Sandbox Code Playgroud)
• 在$HOME/.agda/defaults我有：

  standard-library
  

  Run Code Online (Sandbox Code Playgroud)