Re: [isabelle] locale extension and type variables



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 at … vs first.name at …)

Thanks a lot for the answers, everything works fine !

H.

----- Mail original -----
> De: "Christian Sternagel" <c.sternagel at gmail.com>
> À: cl-isabelle-users at lists.cam.ac.uk, "henri debrat" <henri.debrat at loria.fr>
> Envoyé: Mardi 11 Février 2014 14:10:16
> Objet: 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.