Brian Huffman wrote:
*My* first idea was that "typedef" didn't need to be defining a set
constant at all.
(I would appreciate if we could keep this discussion focused. To discuss
typedef, please start a new thread.)
Makarius wrote:
When we speak about "users" of packages it covers both ML and Isar
theory sources, e.g. the function package is a user of the inductive
package. It is important to keep modularity here.
The system is able to distinguish between things that are visible in the
source vs. internal uses of the same specifciation mechanisms to some
extent, but one needs to look very closely at that when modifying the
behaviour here.
I think there is a formal difference here that is beyond "Isar" vs. "ML":
a) If function calls inductive, then it is exclusively interested in
getting an inhabitant of a specification in the auxiliary context (which
I nowadays prefer to call the "package context"). Its interpretation in
the target is really arbitrary. Local_Theory.define does this uniformly.
b) A user invocation of inductive via the Isar command does not care
about the package context, which is discarded immediately. Here the
target is what counts. In particular, the image in the target is very
irregular at the moment, since the type arguments are only inserted in
very special situations.
It may be worthwhile to make this distinction explicit somehow, but I
want to do a bit of reading before suggesting a concrete solution.
In general, composability of packages is one of my "favorite" problems.
We are still at the beginning here: whenever a package is used for the
first time by some other code, amusing problems come to light. Maybe at
some point we will arrive at a set of general conventions for modular
packages...
Alex
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
