Idris2中导入目录的含义是什么？解析特殊import用法

Idris的模块导入规则里存在一个隐含的文件结构约定，你看到的“导入目录”写法本质是这个约定的体现：

• 当你写import Text.Lexer时，Idris会自动去源码搜索路径下查找Text/Lexer/Core.idr文件——如果某个目录下存在名为Core.idr的文件，这个目录的名称就可以作为该模块的简写入口，导入目录名等价于导入该目录下的Core.idr模块。
• 你遇到的场景里，Text.Lexer目录仅包含Core.idr，所以import public Text.Lexer完全等价于import public Text.Lexer.Core。
• 这里的public修饰符作用和普通导入一致：会把Text.Lexer.Core里的公开符号导出到当前模块的命名空间，其他导入当前模块的代码能直接使用这些符号。

这种约定在社区项目里比较常见，目的是让模块结构更清晰——把相关逻辑放在同一目录下，用Core.idr作为该目录模块的统一入口，只是官方文档没专门提及这个细节。

内容的提问来源于stack exchange，提问作者thor