忽略 Isabelle 中缺失的模式

Question

例如，我想定义一个提取列表第一个元素的函数。对于这个函数，我不关心列表为空的情况（例如，我可以确保每次使用该函数时，我都会传递一个非空列表）。但伊莎贝尔会警告这一点

Missing patterns in function definition:
extracts [] = undefined

我该如何处理这种情况？

Answer 1

您有很多可用的选项，例如：

1. fun extracts where "extracts xs = hd xs"
2. definition extracts where [simp]: "extracts = hd"
3. fun extracts where "extracts xs = (case xs of (x # _) ⇒ x)"
4. fun extracts where "extracts (x # _) = x" | "extracts [] = undefined"