code-generation - 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