Re: [isabelle] New AFP theory: List Index
On Sun, 21 Feb 2010, Brian Huffman wrote:
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.
There are already well-established concepts of long names, name bindings,
naming context, name spaces, which are used everywhere except for the
theory database. So one merely needs to make theories conform to the
established scheme, and somehow link up with the theory loader.
All of this is completely non-trivial.
Nonetheless, it should happen eventually, and without putting the system
into an undefined state.
This archive was generated by a fusion of
Pipermail (Mailman edition) and