[isabelle] Code export, type_synonym, any way to preserve?

Dear All,

I'm exporting to OCaml from Isabelle/HOL. I would like type synonyms to be
preserved (because I perform some munging on the generated code). Is this
possible? The top of the isabelle .thy looks like:

theory Export_code
imports Find Insert Delete Insert_many

export_code "Code_Numeral.nat_of_integer" "Code_Numeral.int_of_integer"



A related question: The code contains eg:

let rec dest_lista
  xs = (match xs
         with [] ->
           failwitha ['d'; 'e'; 's'; 't'; '_'; 'l'; 'i'; 's'; 't'; '\039';
' ']
         | _ :: _ -> (List.butlast xs, List.last xs));;

In Isabelle, the param to failwitha is a string. How can I make the list of
chars param in the generated code a proper OCaml string?

Similarly, my exported code contains things like:

  val split_at : Arith.nat -> 'a list -> 'a list * 'a list

How can I get OCaml's "int" type instead of Arith.nat?



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