Isabelle

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

您可以在吊运包中登记型号。然后 code-generation 工作。此外，不直接使用 Rep_point 而是使用 lift_definition 是有用的，例如，在下面的代码中

setup_lifting type_definition_point

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

export_code xCoord in Haskell module_name Example

Isabelle - 代码生成 - typedef

Isabelle - Code generation - typedef

code-generation