Re: [isabelle] New AFP theory: List Index



On Sun, Feb 21, 2010 at 12:55 AM, Peter Lammich
<peter.lammich at uni-muenster.de> wrote:
> One of the top-candidates on my wish list
> is something like import-qualified, giving the user control over what
> symbols (and syntax) will be loaded into the toplevel-namespace.

Yes!

Besides the flat module namespace, I think that syntax clashes are the
other big obstacle to sharing Isabelle libraries. I have experienced
this problem from both sides.

As a user importing other Isabelle libraries, I have often been
constrained in the choice of syntax to use for my own theories,
because so many useful bits of syntax are already taken by something
in Isabelle/HOL. For example, if I use "_ [_ / _]" as a notation for
substitution in one of my own theories, this causes ambiguous parse
warnings, due to clashes with the List library. This is especially
annoying when my theory does not use lists at all!

As an implementer of Isabelle libraries, adding special syntax for
constants is quite worrisome: What if the end-user of this library is
already using the same syntax for something else? This is the reason
why RealVector.thy doesn't define the standard "||x||" syntax for
"norm x" (I tried adding it once, but it clashed with another
library), and Library/Inner_Product.thy doesn't define an infix-dot
notation for the inner product.

Of course, I can always define nice syntax to use within the library
itself, and then use "no_syntax" at the end to avoid potential clashes
with user theories. But some users might actually want to use my
syntax! It seems silly to have the *library* decide for all users
whether or not some bit of syntax will be visible to them. Obviously,
this choice should left to each user of the library, as Peter
suggests.

- Brian





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