*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] New AFP theory: List Index*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Sun, 21 Feb 2010 07:46:52 -0800*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>, Tobias Nipkow <nipkow at in.tum.de>, Simon Winwood <sjw at cse.unsw.edu.au>*In-reply-to*: <4B80F4FC.8020300@uni-muenster.de>*References*: <4B803BB1.6000907@in.tum.de> <D5B95A2A-767C-40A5-8A97-B2A67A744057@cse.unsw.edu.au> <4B80EA88.8090500@in.tum.de> <4B80F4FC.8020300@uni-muenster.de>*Sender*: huffman.brian.c at gmail.com

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

**Follow-Ups**:**Re: [isabelle] New AFP theory: List Index***From:*Florian Haftmann

**Re: [isabelle] New AFP theory: List Index***From:*Makarius

**References**:**[isabelle] New AFP theory: List Index***From:*Tobias Nipkow

**Re: [isabelle] New AFP theory: List Index***From:*Simon Winwood

**Re: [isabelle] New AFP theory: List Index***From:*Tobias Nipkow

**Re: [isabelle] New AFP theory: List Index***From:*Peter Lammich

- Previous by Date: Re: [isabelle] New AFP theory: List Index
- Next by Date: [isabelle] Why is 'auto' slow here?
- Previous by Thread: Re: [isabelle] New AFP theory: List Index
- Next by Thread: Re: [isabelle] New AFP theory: List Index
- Cl-isabelle-users February 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list