在Idris2中导入目录是什么意思？

Question

我通常会看到 Idris 中的

import

指令用在

.idr

文件上。但在此处的代码中，我看到在目录上使用了

import

的实例。

import public Text.Lexer

，其中 Text.Lexer 是仅包含一个名为

Core.idr

.

的文件的目录

我找不到此类用法的文档。 教程似乎没有说可以导入目录，或者它意味着什么。

有人可以帮忙解释一下目录中导入指令的含义吗？

Answer 1

此存储库中还有一个 file

Text/Lexer.idr

。

import Text.Lexer

只需导入此单个文件。无法导入目录。

在 Idris 和相关语言中，同时具有模块

A

和嵌套在

A

下的某些模块是很常见的。语言不强加任何关系；这样做纯粹是为了组织目的。