In Idris, how do I hide something defined in Prelu

问题:

I want to define my own version of fib to play around with, but fib is exported by the Prelude. How do I hide the import from the Prelude? In Haskell I would write import Prelude hiding (fib), but that doesn't work in Idris.

回答1:

As this Idris mailing post suggests:

At the minute, all there is the (as yet undocumented) %hide directive, which makes a name inaccessible.

Here is an example:

%hide fib

fib : Nat -> Nat
fib Z = Z
fib (S Z) = S Z
fib (S (S n)) = fib n + fib (S n)