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