我正在尝试从一个非常简单的 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
反正我不明白。究竟缺少什么？
最佳答案
您可以在提升和传输包中注册类型。然后代码生成工作。此外，最好不要直接使用 Rep_point , 但要使用 lift_definition相反，例如，如下面的代码。
setup_lifting type_definition_point
lift_definition xCoord :: "point ⇒ real" is fst .
export_code xCoord in Haskell module_name Example
关于code-generation - Isabelle - 代码生成 - typedef，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/34731499/