我知道有一种方法可以使用 %hide 隐藏导入库中的函数。但它似乎不适用于数据类型名称,例如 Nat 和 Vect。有没有办法隐藏数据类型名称,或者只是不导入标准库?
最佳答案
有几个相关的命令行选项:
$ man idris
...
--nobasepkgs Do not use the given base package
--noprelude Do not use the given prelude
--nobuiltins Do not use the builtin functions
...
例如:
$ idris
Idris> :t Nat
Nat : Type
$ idris --noprelude
Idris> :t Nat
No such variable Nat
关于import - Idris:隐藏标准库中的数据类型,或不导入标准库,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/43937149/