Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals

Hi Gottfried,

> consts nat_of :: "'a => nat"
> abbreviation (input) nat_of_int :: "int => nat" where
>   "nat_of_int == nat"
> defs (overloaded)
>   nat_of_int_def [simp,code_unfold]: "nat_of == nat_of_int"

without having had a closer look, I guess your problem is due to that
ad-hoc overloading; the code generator only supports Haskell-style
overloading with type classes.

> value "foo_g(Foo_d2(1::int))"

If the output of »value t« surprises you, the first step is something like

  "blubb = t"

export_code blubb in SML file …

and inspecting the resulting code.

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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