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

> For integers, there's integer in the theory Code_Target, but this maps to
> Big_Int, not it. Many years ago, there was also some setup to implement nat
> with the Big_Int type, but that has long gone, because it was not formally
> checked that all functions maintain the invariant ">= 0". If you import
> Code_Target_Nat from HOL/Library, your generated code will implement
> Arith.nat using Big_Int, so you can construct such Arith.nat values in your
> hand-written code and pass it to functions like split_at.
> As OCaml's int type is bounded, one should not use it for nat, because nat
> is unbounded in HOL. My AFP entry Native_Word imports various fixed-length
> integers from the target languages (OCaml's int as Uint.uint). But clearly,
> Uint.uint is not isomorphic to nat.
Suppose I know somehow (!) that integer overflow is not a problem, and in
OCaml I define a Nat module, with type t = int, which maintains the >=0
invariant (and others? basically, int is made to behave like nat). Is it
possible to target the Nat.t type in Isabelle code generation?


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