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.




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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