In Idris, how do I hide something defined in Prelude?

Question

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.

Accepted Answer

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)
```

In Idris, how do I hide something defined in Prelude?

Solution

Problem