Re: [isabelle] type variable and locales extension



Hi Henri,

A similar problem has been discussed already in 2011
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-November/msg00023.html

Hope this helps
Andreas

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
begin
locale M1 =
fixes getval::"'msg ⇒ 'val"
begin
end


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


end




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,
H.






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