CODEWITHSUNDEEP
importidrisinformation-hiding
Liisi
Liisi

Reputation: 339

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

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?

Upvotes: 2

Views: 210

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15404

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

Upvotes: 3

Related Questions