我遵循Idris 2中的TDD手册,在线文件给出了以下建议:
对于练习4中的
VList
视图,在第10-2章之后,从contrib
库导入Data.List.Views.Extra
。
所以我把这个导入放到一个源文件中(example.idr
)
import Data.List.Views.Extra
但是运行idris2 example.idr
失败了
Error: Module Data.List.Views.Extra not found
我相信控制库的安装是正确的,因为contrib (0.5.1)
出现在idris2 --list-packages
打印的列表中。
如何使Idris 2能够接受来自contrib库的导入?
发布于 2022-05-01 07:00:59
发布于 2022-04-28 11:08:28
idris2二进制文件接受--package
或-p
参数作为依赖项添加包。
使用idris2 -p contrib example.idr
调用解释器可以正确解析导入。
https://stackoverflow.com/questions/72042512
复制相似问题