Re: [isabelle] type variable and locales extension

Hi Henri,

A similar problem has been discussed already in 2011

Hope this helps

On 10/02/14 14:00, Henri Debrat wrote:

Hi all,

There is something about type variables and locales extension that I do not understand.

Here is some test file (the output follows) to illustrate my problem:

theory Test
imports Main
locale M1 =
fixes getval::"'msg ⇒ 'val"

locale M2 = M1 +
fixes setval::"'val⇒'msg"
begin end
print_locale M1
print_locale M2


The first print_locale gives alright:

locale M1
fixes getval :: "'msg ⇒ 'val"

But the second one gives:

locale M2
fixes getval :: "'a ⇒ 'b"
and setval :: "'val ⇒ 'msg"

What I would like it to have the same types in both of the two functions ! I would like to read:

locale M2
fixes getval :: "''val ⇒ 'msg"
and setval :: "'val ⇒ 'msg"

Any clue ?
Thanks in advance,

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