Idris：从标准库中隐藏数据类型，或者不导入标准库

【问题标题】：Idris: Hiding data types from standard library, or not importing standard libraryIdris：从标准库中隐藏数据类型，或者不导入标准库
【发布时间】：2017-10-11 17:44:28
【问题描述】：

我知道有一种方法可以使用 %hide 从导入的库中隐藏函数。但它似乎不适用于数据类型名称，如 Nat 和 Vect。有什么方法可以隐藏数据类型名称，或者只是不导入标准库？

【问题讨论】：

idris --noprelude 阻止导入标准库。
谢谢，这正是我要找的。span>

标签： import idris information-hiding

【解决方案1】：

有几个相关的命令行选项：

$ 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

【讨论】：