Функция двойной список в Isabelle

Question

Я хотел бы определить функцию в Isabelle/хол, которая удваивает список

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

На вашем входе имеется несколько лишних скобок. Обратите внимание, что в отличие от неофициального математического текста (с неофициальным, что означает , как на бумаге;)) в Изабель вы не можете использовать скобки [, ] для явного гнездования. Вместо этого попробуйте следующее.

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