Idris2中的"使用导入"或"隐藏导入"

Question

我想将Control.App导入到一个模块中，该模块在很多地方通过非限定名称PrimIO引用PrimIO.PrimIO。当然，问题是Control.App还导出了一个名为PrimIO的定义。我想通过从Control.App中导入仅App或除PrimIO之外的所有内容来将损害降至最低；即在Haskell中对CCD_ 9或CCD_。

Idris2做这件事的方法是什么？

Answer 1

根据@michaelmesser的评论，我能够用以下方法实现这一点：

import Control.App
%hide Control.App.PrimIO

然而，当我确实需要引用Control.App.PrimIO时，这并不能给我一个明确引用它的好方法。