除了可以在文件系统(带有EMACS,终端等)上使用Agda之外,还可以直接从Haskell作为库使用它吗?例如:
Instead of using Agda on a filesystem (with EMACS, terminal, etc.), is it possible to use it directly from Haskell, as a library? For example:
-- 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,因为该Agda代码上的true : Bool.
The code above would output Bool, because true : Bool on that Agda code.
推荐答案是的,有可能. Agda被设计为Haskell库和一个主要模块.
Yes, it is possible. Agda was designed as a Haskell library plus a main module.
您可以在此处看到几个小示例.作为一个更大的例子,我写了 Apia (无耻插件),它使用Agda作为库.
You can see a couple of small examples here. As a bigger example, I wrote Apia (shameless plug), which uses Agda as a library.
请记住,当前 Agda 说明说:
Please keep in mind that the current Agda description says:
请注意,Agda软件包不遵循软件包版本控制 政策,因为它不打算由第三方程序包使用.
Note that the Agda package does not follow the package versioning policy, because it is not intended to be used by third-party packages.
当然,它可能会改变.
更多推荐
可以将Agda用作库吗?
发布评论