Re: [isabelle] Code generation for sorts from locales
On 16.09.2012 17:34, Florian Haftmann wrote:
I see. At least one out of three keywords in the title of my email was
your experience boils down to the following
definition foo :: "'a ⇒ 'b ⇒ 'b"
where "foo x = id"
"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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and