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

Question

我想知道是否有人可以解决 Agda 中的以下问题。我想将一个自然数 n 作为参数传递给 Agda 模块。在此模块中，我构造了一个函数，该函数采用 Fin n 类型的参数。当模式与该函数的参数匹配时，我遇到的问题是 n 可能是 0，因此类型 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₁ ，其中相关变量已被泛化，然后用于获取 isZero2

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缓冲区中。