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

Question

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

Answer 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