Isabelle - генерация кода - typedef

Question

Я пытаюсь сгенерировать код из очень простой программы Isabelle.

typedef point = "{p::(real*real). True}" by(auto) 
definition xCoord :: "point ⇒ real" where "xCoord P ≡ fst(Rep_point P)" 

export_code xCoord in Haskell module_name Example file code 

но получаю ошибку:

No code equations for Rep_point 

в любом случае я не понимаю. Что именно отсутствует?

Answer 1

Вы можете зарегистрировать тип в подъемно-транспортной упаковке. Затем работает генерация кода. Более того, полезно не использовать непосредственно Rep_point, а вместо этого использовать lift_definition, например, как в следующем коде.

setup_lifting type_definition_point 

lift_definition xCoord :: "point ⇒ real" is fst . 

export_code xCoord in Haskell module_name Example