*To*: Randy Pollack <rpollack at inf.ed.ac.uk>*Subject*: Re: [isabelle] Type parameters in a locale? Datatypes in a locale?*From*: Makarius <makarius at sketis.net>*Date*: Sat, 25 Jun 2011 10:46:53 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <BANLkTinbst3EUdbXQYOOvFB-+ZrwCMzLfA@mail.gmail.com>*References*: <BANLkTinbst3EUdbXQYOOvFB-+ZrwCMzLfA@mail.gmail.com>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Fri, 24 Jun 2011, Randy Pollack wrote:

In the locale context I want to define a datatype datatype ('a,'b) expr = ... where 'a and 'b are the type variables of the locale, and 'a is the lattice. It seems that datatype definitions are not accepted in a locale context, so I defined ('a,'b) expr before the locale and tried to instantiate it with 'a and 'b inside the locale. type_synonym exp = "('a,'b) expr" This fails: '*** Extra variables on rhs: "'b", "'a"'. In my mind, the type variables 'a and 'b are somehow fixed in the locale context, so are not extra variables on rhs.

I try something else: type_synonym ('a,'b) exp = "('a,'b) expr" This fails too: '*** Locally fixed type arguments "'a", "'b" in type declaration "exp"' So Isabelle also thinks 'a and 'b are fixed in the locale context.

That is, in any (concrete?) instance of the locale 'a and 'b will befixed, so I should be able to give them symbolic names and use them asif they were declared (say with typedecl) inside the locale context.

Now I'm stuck. Can I do what I'm trying to do.? If not, is there alogical reason why not?

Makarius

**References**:**[isabelle] Type parameters in a locale? Datatypes in a locale?***From:*Randy Pollack

- Previous by Date: [isabelle] Type parameters in a locale? Datatypes in a locale?
- Next by Date: Re: [isabelle] Type parameters in a locale? Datatypes in a locale?
- Previous by Thread: [isabelle] Type parameters in a locale? Datatypes in a locale?
- Next by Thread: Re: [isabelle] Type parameters in a locale? Datatypes in a locale?
- Cl-isabelle-users June 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list