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"
First question: which type variable of the locale "label" ('a or 'b,
or neither) is understood to be the single type variable of
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and