связывания в Isabelle

Question

При входе следующего определения

datatype env = "nat => 'a option" 

Isabelle/jedit Bad имени показывает восклицательный знак и говорит

Legacy feature! Bad name binding: "nat => 'a option" 

Что такая проблема и как я могу исправить этот синоним типа?

Update: даже

datatype 'a env = "nat => 'a option" 

который лучше определение в теории не решить эту проблему.

Answer 1

С правой стороны определения datatype вы обычно указываете конструкторы типа данных. В вашем примере вы не написали никакого конструктора, поэтому datatype считает, что вы хотите называть его nat => 'a option, что не является юридическим именем для конструктора или любой другой константы Изабеллы.

Если вы хотите ввести env в качестве аббревиатуры от nat => 'a option, type_synonym - это то, что вы ищете.

type_synonym 'a env = "nat => 'a option" 

Обратите внимание, что вам нужно повторить все переменные типа с левой стороны. Затем 'a env и nat => 'a option могут использоваться взаимозаменяемо. Если вы хотите, чтобы ввести новый конструктор типа для env, то вы должны указать имя конструктора, такие как Env:

datatype 'a env = Env "nat => 'a option"