如何解决 Agda 模块参数不灵活的问题？

Question

我想知道是否有人可以解决 Agda 中的以下问题。我想将一个自然数 n 作为参数传递给 Agda 模块。在这个模块中，我构造了一个接受Fin n 类型参数的函数。当模式与此函数的参数匹配时，我得到n 可能是zero 的问题，因此Fin n 类型将为空。 Agda 不会接受 Fin n 的 zero 和 suc _ 构造函数。

奇怪的是，当你在函数本身中引入原始自然数时，Agda 似乎没有这个问题，并且函数编译正常。

下面是一个最小的例子：

open import Data.Nat
open import Data.Fin
open import Data.Bool

module Test (n : ℕ) where

  -- Compiles
  isZero₁ : ∀ {m : ℕ} → Fin m → Bool
  isZero₁ zero = true
  isZero₁ (suc _) = false

  -- Does not compile with error: "suc n₁ != n of
  -- type ℕ when checking that the pattern zero has type Fin n"
  isZero₂ : Fin n → Bool
  isZero₂ zero = true
  isZero₂ (suc _) = false

在真正的模块中，我传入了 5 个其他参数，这些参数依赖于 n。因此我确实需要提供n 作为参数。同时，我还需要能够编写模式匹配Fin n 类型对象的函数。有人知道我该怎么做吗？

Answer 1

Ulf 今天一直在努力解决该特定问题。它应该很快就会登陆master。同时，您必须定义isZero₁，其中有问题的变量已被泛化，然后用于获取isZero₂

isZero₂ : Fin n → Bool
isZero₂ = isZero₁

因为为更通用的函数写下类型可能有点烦人，您可以使用C-c C-h，它可以帮助您生成辅助函数的类型。写isZero 但不填写正文，进入洞，输入辅助函数的名称和您希望将其应用于的参数，然后C-c C-h 将为您生成一个类型。例如，给定源文件：

isZero : Fin n → Bool
isZero = {! auxiliary !}

如果你进入这个洞并输入C-c C-h，你会得到：

auxiliary : ∀ {n} → Fin n → Bool

在AgdaInfo 缓冲区中。