Re: [isabelle] New AFP theory: List Index



> A feature that I often miss, especially considering namespace pollution
> problems. 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.

This is a misunderstanding which exhibits the source of the problem:
syntax is not bound to namespaces but always global, which makes
pollution pervasive (c.f. the funny (no_)notation declarations for inf
and sup in the HOL theories -- an Isabelle joke...). We need finer
control over syntax here.

> Currently, the hide-command allows one to hide
> private symbols, but the other way round would be more comfortable.

I do not seed this demand as urgent: given that theory developers have
thought carefully which symbols ought to be hidden / qualified, the user
is always free to hide additional symbols when needed.

> If users want hierarchical module names, why don't we (the Isabelle
> developers) just implement that feature?

I agree that this is desirable.  But I suppose we first should find a
way to replace the rather archaic session concept by something which is
less driven by building descriptions in IsaMakefiles and ROOT.MLs, but
by the implicit structure of hierarchies.

A somehow related question is how to treat relative imports.  I recall
there has been (still is?) much debate on this in the Java and Python
community, and this has to be considered carefully (maybe inspired by
Scala!?).


Tapping yet another barrel... ;-)
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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