是否可以使用 Agda 作为库？

是否可以直接从 Haskell 将其用作库，而不是在文件系统（使用 EMACS、终端等）上使用 Agda？例如：

-- UsingAgda.hs
import Agda

-- Prints the type of a term on some Agda code
main :: IO ()
main = typeOf "true" agdaCode where

  agdaCode :: String
  agdaCode = unlines
    ["module Hello where   "
    ,"                     "
    ,"data Bool : Set where"
    ,"  true  : Bool       "
    ,"  false : Bool       "]

上面的代码将输出Bool， 因为true : Bool在 Agda 代码上。

对的，这是可能的。 Agda 被设计为一个 Haskell 库加上一个主模块。

你可以看几个小例子here。作为一个更大的例子，我写了Apia（无耻插件），它使用Agda作为库。

请记住，current Agda 描述 says:

请注意，Agda 包不遵循包版本控制 策略，因为它不打算被第三方包使用。

当然，它可能会改变。