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