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 MHonArc.