进入 Agda 标准库的根目录，并发出以下命令：
grep -r "module _" . | wc -l
产生以下结果：
843
每当我遇到这样的匿名模块（我假设这就是它们的名字）时，我完全无法弄清楚它们的目的是什么，尽管它们明显无处不在，也不知道如何使用它们，因为根据定义，我无法使用他们的名字，尽管我认为这应该是可能的，否则即使允许定义它们也是没有意义的。
维基页面：
https://agda.readthedocs.io/en/v2.6.1/language/module-system.html#anonymous-modules
有一个名为“匿名模块”的部分实际上是空的。
有人可以解释一下匿名模块的目的是什么吗？
如果可能，任何强调此类模块定义的相关性以及如何使用其内容的示例将非常感激。
以下是我提出的可能的想法，但似乎没有一个是完全令人满意的：
private）。匿名模块可用于简化共享某些参数的一组定义。例子：
\nopen import Data.Empty\nopen import Data.Nat\n\n<\xe2\x87\x92\xc2\xac\xe2\x89\xa5 : \xe2\x88\x80 {n m} \xe2\x86\x92 n < m \xe2\x86\x92 n \xe2\x89\xa5 m \xe2\x86\x92 \xe2\x8a\xa5\n<\xe2\x87\x92\xc2\xac\xe2\x89\xa5 = {!!}\n\n<\xe2\x87\x92> : \xe2\x88\x80 {n m} \xe2\x86\x92 n < m \xe2\x86\x92 m > n\n<\xe2\x87\x92> = {!!}\n\nmodule _ {n m} (p : n < m) where\n\n <\xe2\x87\x92\xc2\xac\xe2\x89\xa5\xe2\x80\xb2 : n \xe2\x89\xa5 m \xe2\x86\x92 \xe2\x8a\xa5\n <\xe2\x87\x92\xc2\xac\xe2\x89\xa5\xe2\x80\xb2 = {!!}\n\n <\xe2\x87\x92>\xe2\x80\xb2 : m > n\n <\xe2\x87\x92>\xe2\x80\xb2 = {!!}\n据我所知，这是匿名模块的唯一用途。当module _作用域关闭时，您无法再引用该模块，但您可以引用其定义，就好像它们根本没有在模块中定义一样（但使用了额外的参数）。