Re: [isabelle] Code generation for sorts from locales



Hi Florian,

On 16.09.2012 17:34, Florian Haftmann wrote:
your experience boils down to the following

definition foo :: "'a ⇒ 'b ⇒ 'b"
   where "foo x = id"

lemma [code]:
   "foo (x :: 'a) = (id :: 'a ⇒ 'a)"
   by (simp add: foo_def)

export_code foo in Haskell
i.e. currently the code generator accepts code equations which violate
the precondition that the type scheme of the constant in the theorem
(here, 'a => 'a => 'a) must match to the type scheme of the constant in
the theory (here, 'a => 'b => 'b).  I will have to investigate this and
to repair the corresponding check.
I see. At least one out of three keywords in the title of my email was appropriate :-)
Note that in order for your example to work, you must generalize your
interpretation to let A.my_code have a suitable type scheme for my_code.
I have restricted the type of my_code instead and it works.

Thanks!

Dmitriy





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