在 Idris 中，如何隐藏 Prelude 中定义的内容？
In Idris, how do I hide something defined in Prelude?
我想定义我自己的 fib 版本来玩，但是 fib 是由 Prelude 导出的。如何从 Prelude 中隐藏导入？在 Haskell 中我会写 import Prelude hiding (fib)，但这在 Idris 中不起作用。
正如这个 Idris 邮件 post 所建议的那样：
At the minute, all there is the (as yet undocumented) %hide directive, which makes a name inaccessible.
这是一个例子：
%hide fib
fib : Nat -> Nat
fib Z = Z
fib (S Z) = S Z
fib (S (S n)) = fib n + fib (S n)
我想定义我自己的 fib 版本来玩，但是 fib 是由 Prelude 导出的。如何从 Prelude 中隐藏导入？在 Haskell 中我会写 import Prelude hiding (fib)，但这在 Idris 中不起作用。
正如这个 Idris 邮件 post 所建议的那样：
At the minute, all there is the (as yet undocumented)
%hidedirective, which makes a name inaccessible.
这是一个例子：
%hide fib
fib : Nat -> Nat
fib Z = Z
fib (S Z) = S Z
fib (S (S n)) = fib n + fib (S n)