`import using` or `import hiding` in Idris2

user_477476 0
Viewed 133

I'd like to import Control.App into a module that refers to PrimIO.PrimIO via the unqualified name PrimIO in a lot of places. The problem, of course, is that Control.App also exports a definition named PrimIO. I would like to minimize the damage by importing either only App or everything but PrimIO from Control.App; i.e. what one would do with import Control.App (App) or import Control.App hiding (PrimIO) in Haskell.

What is the Idris2 way of doing this?

idris import syntax namespaces module
1 Answers

Based on @michaelmesser's comment, I was able to get this working with the following:

import Control.App
%hide Control.App.PrimIO

However, this doesn't give me a good way of explicitly referring to Control.App.PrimIO when I do need to refer to it.

user_4774760
Related