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.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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