Email Gateway (Aug 19 2022 at 13:47): Email Gateway (Aug 19 2022 at 13:47):From: Henri Debrat <henri.debrat@loria.fr>
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.
Email Gateway (Aug 19 2022 at 13:47):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 19 2022 at 13:47):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Henri,
I guess that without having any assumptions over "getval" and "setval"
connecting the both, what you experience might be the expected result.
To give such a connection explicitly, you can use:
locale M2 =
M1 getval for getval :: "'msg => 'val" +
fixes setval :: "'val => 'msg"
begin
end
cheers
chris
Last updated: Oct 31 2025 at 20:23 UTC