# Re: [isabelle] Type parameters in a locale? Datatypes in a locale?

Quoting Randy Pollack <rpollack at inf.ed.ac.uk>:

Consider the following in HOL
locale label = bounded_lattice +
fixes lblRem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
and canElim :: "'b \<Rightarrow> 'a \<Rightarrow> bool"
begin
First question: which type variable of the locale "label" ('a or 'b,
or neither) is understood to be the single type variable of
"bounded_lattice"?

`This is not specified. Use print_locale to find out what happened
``(you may need to set show_types).
`

I want 'a to be the lattice. How can I say that?

`You need to mention the type variable in the imported expression.
``This can be done like this:
`
locale label = bounded_lattice x for x :: "... 'a ..." + ...

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.
[...]
Now I'm stuck. Can I do what I'm trying to do.? If not, is there a
logical reason why not?

As Makarius already said, use ('a, 'b) expr in your locale.
Clemens

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