Idris: Masquage des types de données de la bibliothèque standard, ou non importation de la bibliothèque standard

Question

Je sais qu'il existe un moyen de masquer les fonctions des bibliothèques importées, avec% hide. Mais cela ne semble pas fonctionner sur les noms de types de données, comme Nat et Vect. Est-il possible de masquer les noms de types de données, ou simplement d'importer la bibliothèque standard?

Answer 1

Il y a plusieurs options de ligne de commande pertinents:

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

Par exemple:

$ idris 
Idris> :t Nat 
Nat : Type 

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