Блог

Я пытаюсь понять опции в Isabelle (2020) и не могу понять, почему некоторые простые выражения option не вычисляются или не упрощаются, как ожидалось.

Например, я ожидал бы, что

 value "some (1::nat)"
 

должен возвращать "nat option" тип, однако он возвращает неопределенный тип:

 "some 1"
  :: "'a
 

Более того, исходя из сигнатуры типа, я бы ожидал the , что функция вернет значение «внутри» опции, так что «the (some (1::nat))» — это просто (1::nat) .

Однако,

 value "the (some (1::nat))"
 

возвращает, казалось бы, не очень полезный тип:

 "the (some 1)"
  :: "'a"
 

, чего нет nat . Тогда результат не очень полезен, например

  value "the (some (1::nat))   2"
 

ВОЗВРАТ

 "the (some 1)   (1   1)"
  :: "'a"
 

(Я ожидал, что результат будет "3::nat" )

Это сделано специально, или я что-то упускаю the , или как опции упрощают / вычисляют в Isabelle?

(У меня нет предварительных знаний о параметрах Isabelle, и я просто предполагаю, что это похоже на, может быть, на Хаскелла.)

Щелчок C на показывает, что определение:

 datatype 'a option =
    None
  | Some (the: 'a)
 

Это некоторые, а не некоторые.

Существует подсказка, которая some не определена: цвет не совпадает с цветом из the .