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

definition
  "blubb = t"

export_code blubb in SML file …

and inspecting the resulting code.

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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