在Isabelle中将列表加倍的功能 [英] Function to double a list in Isabelle

问题描述

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

I would like to define a function in Isabelle/HOL that doubles a list

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]"

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

as well as some other definitions. I get the error

类型统一失败

Type unification failed

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

Type error in application: incompatible operand type

我的功能出了什么问题?

What is wrong with my function?

推荐答案

实际上，错误消息包含一些其他信息.即

Actually the error message contains some further information. Namely

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

告诉我们[[x, l]]是?'a list list类型，即列表列表.要将其作为double的参数(需要一个'a list类型的参数)，您会得到类型错误.

which tells us that [[x, l]] is of type ?'a list list, i.e., a list of lists. As you want to give it as argument to double, which expects an argument of type 'a list, you get the type error.

错误消息中术语[[x, l]]的起源是定义的第二行

The origin of the term [[x, l]] in the error message is the second line of your definition

`double [x # [l]]`

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

您的输入中有几个多余的括号.请注意，与Isabelle中的非正式数学文本(非正式意思是在纸上；)相反，您不能使用方括号[，]进行显式嵌套.请尝试以下操作.

There are several superfluous brackets in your input. Note that in contrast to informal mathematical text (with informal meaning as on paper ;)) in Isabelle you cannot use brackets [, ] for explicit nesting. Try the following instead.

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

这篇关于在Isabelle中将列表加倍的功能的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！