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

Idris: Hiding data types from standard library, or not importing standard library

我知道有一种方法可以使用 %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