Re: [isabelle] Bug report: Locale parameters are not visible



On Tue, Dec 21, 2010 at 2:52 PM, Victor Porton <porton at narod.ru> wrote:
> The following theory does not verify. I consider this a bug of Isabelle 2009-2.

> locale loc =
>  fixes "x"
>
> interpretation inter: loc "0" .
>
> definition "a == inter.x"

You might call this a "feature request" rather than a "bug report".
The locale tutorial says that qualified names are generated for
*definitions* in a locale, but it says nothing about generating
qualified names for the *parameters* of the locale.

Anyway, considered as a feature request, this actually seems pretty
reasonable to me. And it seems like it wouldn't be too hard to
implement.

> locale loc =
>  fixes "x"
> begin
>
> definition "x1 == x"
>
> end
>
> interpretation inter: loc "0" .
>
> definition "a == inter.x1"

Currently, the locale interpretation above introduces "inter.x1" as an
input abbreviation for "loc.x1 0". We could also introduce "inter.x"
as an input-only abbreviation for "0".

I don't think such a feature would cause any backward-compatibility
problems. Does anyone have any objections or other comments?

- Brian





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