相关疑难解决方法(0)

而不是在文件系统上使用Agda(使用EMACS,终端等),是否可以直接从Haskell使用它作为库？例如:

-- 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代码上.