Re: [isabelle] String.explode in generated code



Hi Andreas,

first, the appropriate solution to your problem should be

code_modulename SML
  String Stringa

> In Isabelle2009-2, the code generator translated the theory String into
> the module Stringa. In Isabelle2011, it uses String. 
> 
> Surprisingly, with the @{code} antiquotation, everything seems to work
> fine.

The reason is that all runtime services uses target language Eval rather
than SML (as noted in code generation tutorial p. 31) and typically do
not use different structures.

After some experimentation I have a feeling that code_reserved does not
exactly behave as expected, I will keep track on this.

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.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.