Partial import of modules?

[Dirk Ullrich]

Hello Edwin,

sometimes it would be very convenient to import a module foo, but to
use only some of foo's definitions. So is there any way in Idris to
select / hide definitions when importing a module? Otherwise such a
mechanism - even a very simple one - would be one of my top
nice-to-haves for Idris.

Dirk

[Edwin Brady]

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

I'll add it to my TODO list - it shouldn't be too hard to do.

Incidentally, it'd probably be useful if my TODO list was public in some kind of bug/issue tracker. Does anyone have any recommendations? Otherwise I'll just start using the github one...

Edwin.

[Ramana Kumar]

the github one is good

[Dirk Ullrich]

Hi

Am 27. Februar 2012 18:46 schrieb Ramana Kumar <ramana...@gmail.com>:
> the github one is good
>

+1

> On Feb 27, 2012 3:01 PM, "Edwin Brady" <edwin...@gmail.com> wrote:

[...]

>> Incidentally, it'd probably be useful if my TODO list was public in some
>> kind of bug/issue tracker. Does anyone have any recommendations? Otherwise
>> I'll just start using the github one...
>>
>> Edwin.
>>

[...]
Dirk