[isabelle] OCaml code generator problem: Big_int



Hi,
the Ocaml code generator generates the following lines of (invalid)
OCaml-Code. Note that I'm using Efficient_Nat:

module Integer =
struct

let rec suc n = Big_int.add_big_int n 1;;

OCaml complains:

File "generated/Ta.ml", line 31, characters 38-39:
Error: This expression has type int but an expression was expected of type
         Big_int.big_int

I do not know much about OCaml, but I suspect there is some missing
type-coercion.

Is there any fix to get correct generated code?

Many thanks in advance and regards,
  Peter lammich








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