[isabelle] Code export, type_synonym, any way to preserve?
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:
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