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.