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:
> Tobias Nipkow wrote:
>> A complication is that Isabelle does not support hierarchical module
>> names in the way Haskell (or Java or ...) does.
> A feature that I often miss, especially considering namespace pollution
If users want hierarchical module names, why don't we (the Isabelle
developers) just implement that feature?
The implementation wouldn't involve much:
1. Make the dot "." a legal character in module names.
2. Define a new mapping from module names to filepaths, so that
"imports A.B.C" makes Isabelle load the file "~/A/B/C.thy", where "~"
is filled in with some directory from the search path.
The hard part would be social, rather than technical: Deciding how to
organize and populate the hierarchy. But we wouldn't have to switch
over everything at once---we could flesh out the hierarchy gradually,
with input from the user community, and move libraries to their new
places in the namespace one at a time. I think this would work, and
solving the problem of module name clashes would remove one big
obstacle to sharing Isabelle libraries.
This archive was generated by a fusion of
Pipermail (Mailman edition) and