CODEWITHSUNDEEP
code-generationisabelle
LandWab
LandWab

Reputation: 43

Isabelle - Code generation - typedef

I am trying to generate code from a very simple Isabelle-program.

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

but get the error:

No code equations for Rep_point

anyway I do not understand. What exactly is missing?

Upvotes: 4

Views: 548

Answers (1)

René Thiemann
René Thiemann

Reputation: 1271

You can register the type in the lifting and transfer package. Then code-generation works. Moreover, it is useful to not directly use Rep_point, but to use lift_definition instead, e.g., as in the following code.

setup_lifting type_definition_point

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

export_code xCoord in Haskell module_name Example

Upvotes: 4

Related Questions