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

Question

I know there is a way to hide functions from imported libraries, with %hide. But it does not seem to work on data type names, like Nat and Vect. Is there any way to hide data type names, or just not import the standard library?

Answer 1

There are several relevant command-line options:

$ man idris
...
   --nobasepkgs             Do not use the given base package
   --noprelude              Do not use the given prelude
   --nobuiltins             Do not use the builtin functions
...

For instance:

$ idris
Idris> :t Nat
Nat : Type

$ idris --noprelude
Idris> :t Nat
No such variable Nat