在 Isabelle 中将列表加倍的函数

Question

我想在 Isabelle/HOL 中定义一个将列表翻倍的函数

fun double :: "'a list => 'a list" where
...

这样double [x1, x2, ...] = [x1, x1, x2, x2, ...]

我尝试了以下方法：

fun double :: " 'a list ⇒ 'a list" where
"double [] = []" |
"double [x#[l]] = x # x # double [l]"

以及其他一些定义。我得到了错误

类型统一失败

应用程序中的类型错误：操作数类型不兼容

我的功能有什么问题？

Answer 1

实际上，错误消息包含一些进一步的信息。即

Operator:  double :: 'a list ⇒ 'a list
Operand:   [[x, l]] :: ??'a list list

这告诉我们[[x, l]] 是?'a list list 类型，即列表列表。当您想将它作为参数提供给 double（它需要一个类型为 'a list 的参数）时，您会收到类型错误。

错误信息中[[x, l]]这个词的来源是你定义的第二行

`double [x # [l]]`

其中x#[l] 打印为等效的[x, l]。

您的输入中有几个多余的括号。请注意，与 Isabelle 中的非正式数学文本（informal 表示 as on paper ;)）相比，您不能使用括号 [、] 进行显式嵌套。请尝试以下方法。

fun double :: " 'a list ⇒ 'a list"
where
  "double [] = []" |
  "double (x#xs) = x # x # double xs"