[isabelle-dev] Interpretation in arbitrary targets.
ballarin at in.tum.de
Thu Apr 18 22:55:48 CEST 2013
This view is correct, but it is not the whole story. Since the system
maintains a graph of interpretations and follows them transitively,
the effect achieved by
sublocale locale < expression
is much like
instance class < sort
of the old user interface to type classes. This relationship is
discussed in the new paper (Section 5.2).
Quoting Tobias Nipkow <nipkow at in.tum.de>:
> Let me just make some remarks as a user. At ITP 2011 I published a paper
> http://www21.in.tum.de/~nipkow/pubs/itp11.html where I showed how to
> use locales
> to structure stepwise development of modules (see p11). In that context I
> intentionally used the notation
> interpretation (in A) B-expr
> instead of sublocale in an implementation step. Of course I comment on the
> deviation in the notation saying that I have chosen this variation of
> interpretation because it is more intuitive (see p10). I do find it more
> intuitive because it tells me clearly what is going on: some locale
> is interpreted in some locale. And this is also how you explain sublocale in
> your locale tutorial. Hence Florian's suggestions made a lot of sense to me.
> Am 17/04/2013 22:28, schrieb Clemens Ballarin:
>> Quoting Makarius <makarius at sketis.net>:
>>> On Fri, 12 Apr 2013, Clemens Ballarin wrote:
>>>> That sounds a bit dogmatic. If additional commands are made available for
>>>> targets, then the syntax should clearly be more flexible if
>>>> better intuition
>>>> can be achieved.
>>> That is just a matter of modularity of concepts: the older "(in
>>> a)" notation
>>> was slightly generalized at some point to allow named contexts as sketched
>>> above, and the relation between the two is as pointed out by Florian.
>> I am aware of the modularity aspect of this. My criticism is that
>> from the current approach in favour of preferable notation are not even
>> considered. In any case, I'm not sure how useful the old notation still is.
>> Maybe it can be given up at some point.
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev