agda - 我可以使用值的范式来避免 Agda 中不完整的模式匹配吗？

Question

在下面的 Agda 程序中，我收到关于 one 定义中缺少大小写的警告，尽管 myList 仅适合 cons 案例。

open import Data.Nat

data List (A : Set) : Set where
  nil : List A
  cons : A → List A → List A

myList : List ℕ
myList = cons 1 (cons 2 (cons 3 nil))

one : ℕ
one with myList 
... | (cons x xs) = x

Incomplete pattern matching for .test.with-16. Missing
cases:
  one | nil

我知道这听起来有点复杂，但有没有一种方法可以根据 myList 定义 one，而不会遇到“不完整的模式匹配”错误？

这个示例是我原来问题的简化，该问题来自家庭作业，并且使用稍微复杂的类型。在这种情况下，“myList”是一个聪明的函数根据一个小输入计算出的一个大值。如果我使用 Emacs 的 Agda 模式 (C-c C-n) 计算 "myList" 的正常形式，我可以从中获取 "one" 的值并将其粘贴到我的程序。然而，这个值在打印出来时需要几十行，所以我想知道是否有一种方法可以直接用 "myList" 定义 "one" ，而不会遇到不完整的模式匹配错误。

Answer 1

如果您将 与 e 一起使用，则 e 将从目标和上下文中抽象出来(认为是 lambda 抽象)，并且系统会要求您继续，就像那里有一个变量一样而不是 e 本身。因此，下面的模式匹配根本不考虑 myList 的值(这相当违反直觉，但 with 只是用一个额外参数创建辅助定义的语法糖)。

但是您可以编写以下内容:

open import Agda.Builtin.List
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Equality

myList : List ℕ
myList = 1 ∷ 2 ∷ 3 ∷ []

head : {n : ℕ} {ns : List ℕ} (xs : List ℕ) → n ∷ ns ≡ xs → ℕ
head (x ∷ xs) refl = x

one : ℕ
one = head myList refl

您还可以查看标准库中的 inspect 模式，以获得此问题的更通用的解决方案。