主页 / coding / 问题 / 77849572
Accepted
thor
Asked: 2024-01-20 09:46:49 +0800 CST

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

  • 772

我通常会看到importIdris 中的指令用于文件.idr。但在此处的代码import中，我看到一个在目录上使用的实例。

import public Text.Lexer

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

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

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

idris

1 个回答

  1. Best Answer

    该存储库中还有一个文件 Text/Lexer.idr。import Text.Lexer只需导入这个单个文件即可。无法导入目录。

    在 Idris 和相关语言中，一个模块A和一些嵌套在A. 语言不强加任何关系；这样做纯粹是为了组织目的。

    • 2

相关问题