Idris2 中的“导入使用”或“导入隐藏”答案

【问题标题】：`import using` or `import hiding` in Idris2Idris2 中的“导入使用”或“导入隐藏”
【发布时间】：2021-03-25 01:37:48
【问题描述】：

我想将Control.App 导入到一个模块中，该模块在很多地方通过不限定名称PrimIO 引用PrimIO.PrimIO。当然，问题在于Control.App 还导出了一个名为PrimIO 的定义。我想通过从Control.App 导入仅App 或除PrimIO 以外的所有内容，以尽量减少损失；即在 Haskell 中使用 import Control.App (App) 或 import Control.App hiding (PrimIO) 会做什么。

Idris2 的实现方式是什么？

【问题讨论】：

我认为它还没有实现。请参阅github.com/idris-lang/Idris2/wiki/Contributions-wanted 如果您想尽快获得它，您可能需要提交 PR。
%hide 做你想做的事吗？

标签： import syntax module namespaces idris

【解决方案1】：

根据@michaelmesser 的评论，我能够使用以下方法来完成这项工作：

import Control.App
%hide Control.App.PrimIO

但是，当我确实需要引用 Control.App.PrimIO 时，这并没有给我一个明确引用 Control.App.PrimIO 的好方法。

【讨论】：