Re: [isabelle] locale extension and type variables



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

On 02/11/2014 01:32 PM, Henri Debrat wrote:

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.





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