Re: [isabelle] Code generation for "int" in Isabelle 2013-1 RC3

Dear Jesus,

In the upcoming release, target language numerals like are properly encapsulated in their own types integer and natural. Formerly, the adaptation theories made the SML code generator to implement the types nat and int directly as, now Code_Target_Numeral implements both as type copies of to enforce the separation. Consequently, you cannot exploit the former clash of types any more. You have to define an function that operates directly on integer rather than nat. For example:

definition findi_integer ::
  "(integer * 'a => bool) => 'a iarray => (integer * 'a) option"
  "findi_integer f arr = (apfst integer_of_nat) (findi (f o apfst integer_of_nat) arr)"

    constant findi_integer => (SML) "Vector.findi"

Of course, you also have to use findi_integer instead of findi in your code equations or prove a corresponding code equation for findi.

Hope this helps,

On 04/11/13 08:50, Jesus Aransay wrote:
Dear all,

the code generation snippet in the attached file worked in Isabelle
2013 but fails in Isabelle 2013-1 RC3; a function resembling the SML
Vector.findi ( is
introduced in Isabelle, and then serialised to SML Vector.findi, but
apparently there is a clash between the Isabelle code generated
structure "int" and the SML "".

I have tried to import "Code_Target_Int" with similar result.

Is there an easy way to avoid such clash? (I could edit the SML code
by hand and fix types' declarations, but does not seem a proper

Thanks in advance for any advice,


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