Re: [isabelle] Code_reflect with abstract constructor(s)

Hi Wenda,

> 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?

try something like

	code_reflect Foo
	  datatypes rat
	  functions â

where â stands for the operations you actually want to refer to in later
Isabelle/ML sections.

In the upcoming Isabelle release, a new concept called ÂComputationsÂ
has been implemented.  You might want to study the corresponding
sections in the Tutorial on Code Generation; maybe this is a suitable
replacement for your current application of code_reflect.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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