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