module - 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. 他们的内容仅在他们的英语模块内可见/使用(有点像 private block )。

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 _ 范围关闭时，您不能再引用该模块，但您可以引用它的定义，就好像它们根本没有在模块中定义一样(但有额外的参数相反)。