Email Gateway (Aug 19 2022 at 13:49): Email Gateway (Aug 19 2022 at 13:49):From: Henri Debrat <henri.debrat@loria.fr>
Hi all,
Here is the content of 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 is to have the same types in both of the two functions. I would like to get the following output:
locale M2
fixes getval :: "''val ⇒ 'msg"
and setval :: "'val ⇒ 'msg"
Any clue ?
Thanks in advance,
H.
Email Gateway (Aug 19 2022 at 13:49):From: Christian Sternagel <c.sternagel@gmail.com>
This seems to be a duplicate of an earlier message (subject: type
variable and locales extension) that has already been answered. By
Andreas and myself.
Did you try:
locale M2 =
M1 getval for getval :: "'msg => 'val" +
fixes setval :: "'val => 'msg"
begin
end
cheers
chris
Email Gateway (Aug 19 2022 at 13:49):From: Henri Debrat <henri.debrat@loria.fr>
Hi Christian,
Sorry for that. It is a duplicate, indeed. I had some issues with posting to the list (because of the format of my email address, I guess ? name@… vs first.name@…)
Thanks a lot for the answers, everything works fine !
H.
----- Mail original -----
Last updated: Apr 25 2024 at 08:20 UTC