Re: [isabelle] Combining locales?
I like your suggestion. However I guess I didn't understand it.
locale labelAuth =
label: lattice where
le = lblle and lt = lbllt and inf = lblinf and sup = lblsup
auth: lattice where
le = authle and lt = authlt and inf = authinf and sup = authsup
returns error message
*** "le" not a parameter of instantiated expression
*** At command "locale" (line 3 of
I tried a few other syntaxes without success, e.g.
locale labelAuth =
label: lattice where label.le = lblle
*** Outer syntax error (line 4 of
*** but keyword where (line 4 of
I'm completely floundering. I found no explanation I could understand
in the Tutorial on Locales.
On Mon, Nov 14, 2011 at 3:25 PM, Clemens Ballarin <ballarin at in.tum.de> wrote:
> If this resolves the problem, then not only the order of the arguments of
> the locale predicate but also the order of the locale parameters has
> changed. The latter is, of course, not internal if a class is used as a
> Randy can make the locale expression invariant to such changes by using
> named instantiation syntax like this:
> labelAuth =
> label: lattice
> where le = lblle and lt = lbllt and inf = lblinf and sup = lblsup +
> auth: lattice
> Quoting Alexander Krauss <krauss at in.tum.de>:
>> Hi Randy,
>> On 11/14/2011 07:40 PM, Florian Haftmann wrote:
>>> I dimly remember that there have been changes in the type class import
>>> hierarchy which changed the order of arguments for locale predicates,
>>> but I can't recall exactly which. Maybe somebody else can comment?
>> The change was 5e51075cbd97, and here is the NEWS entry:
>> * Added syntactic classes "inf" and "sup" for the respective
>> constants. INCOMPATIBILITY: Changes in the argument order of the
>> (mostly internal) locale predicates for some derived classes.
>> Your definition works again, when lblinf/authinf are moved to the front.
>> The dependence of the predicate arguments on the specifics of the hierarchy
>> is a bit unfortunate...
This archive was generated by a fusion of
Pipermail (Mailman edition) and