Agda 中匿名模块的用途

Question

进入 Agda 标准库的根目录，并发出以下命令：

grep -r "module _" . | wc -l

产生以下结果：

843

每当我遇到这样的匿名模块（我假设这就是它们的名称）时，我完全不知道它们的用途是什么，尽管它们明显无处不在，也不知道如何使用它们，因为根据定义，我无法访问他们的内容使用他们的名字，虽然我认为这应该是可能的，否则他们甚至允许他们被定义是没有意义的。

维基页面：

https://agda.readthedocs.io/en/v2.6.1/language/module-system.html#anonymous-modules

有一个名为“匿名模块”的部分实际上是空的。

有人能解释一下匿名模块的用途是什么吗？

如果可能，任何强调此类模块定义相关性以及如何使用其内容的示例将不胜感激。

---

以下是我想出的可能的想法，但似乎没有一个是完全令人满意的：

1. 它们是一种在 Agda 文件中重新组合主题相同的定义的方法。
2. Agda 在使用它们提供的功能时以某种方式推断出它们的名称。
3. 他们的内容只是为了在他们的 englobing 模块中可见/使用（有点像 private 块）。

Answer 1

匿名模块可用于简化共享一些参数的一组定义。示例：

open import Data.Empty
open import Data.Nat

<⇒¬≥ : ∀ {n m} → n < m → n ≥ m → ⊥
<⇒¬≥ = {!!}

<⇒> : ∀ {n m} → n < m → m > n
<⇒> = {!!}

module _ {n m} (p : n < m) where

  <⇒¬≥′ : n ≥ m → ⊥
  <⇒¬≥′ = {!!}

  <⇒>′ : m > n
  <⇒>′ = {!!}

Afaik 这是匿名模块的唯一用途。当module _ 范围关闭时，您不能再引用该模块，但您可以引用它的定义，就好像它们根本没有在模块中定义一样（而是使用额外的参数）。