Re: [isabelle] type variable and locales extension



Dear Henri,

On 02/10/2014 02:00 PM, Henri Debrat wrote:
locale M2 = M1 +
fixes setval::"'val⇒'msg"
begin end
print_locale M1
print_locale M2

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




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