[isabelle] Code_reflect with abstract constructor(s)



Dear code generation experts,

When porting some of my code from Isabelle2016 to Isabelle2016-1 (as well as the latest repository version:5be0b0604d71), I found that the following piece of code was no longer working:

code_reflect Foo
  datatypes rat=â_"

And the error message said âCannot export abstract constructor(s): Frctâ. 

I understand the idea of abstract constructors that are usually not allowed on the right-hand side of a code equation. Nevertheless, I am a little baffled here and was wondering what is the standard way to circumvent the situation?

Best,
Wenda


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.