On Tue, 29 Nov 2011, Lukas Bulwahn wrote:
On 11/28/2011 10:41 PM, Makarius wrote:
On Mon, 28 Nov 2011, Lukas Bulwahn wrote:
many recent requests for adjusting the user-space behavior of
typedef
would then rather apply to quotient_type.
Also, I do not see the clear advantage how the suggested change would
make the adjustments simpler. I would rather imagine that the
quotient_type command could be assimilated by extending the typedef
command to enable to hook the pre- and post processing of quotient
type into typedef.
This reminds me of datatype interpretation, but it is more like an
example of super package bloat.
The quotient type defines a type with typedef, defines some further
constants, and sets some declarations. If typedef becomes a super
package, all this could be done somewhere in typedef with some setup.
BTW, there is already Typedef.interpretation, which means other packages
can participate in each foundational defition of a typedef -- the internal
name is passed as a handle. This allows to "consolidate" derived content
in the context, e.g. add-on definitions. It also requires some care,
because interpretations refer to all past and future items being
introduced -- a bad interpretation function can easily bomb the theory, in
particular after unexpected merges.
If the augmented content is just a plain function over the existing data,
it is easier to add it to the lookup function of the other package, to
produce extra stuff on the spot in a non-persistent manner.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
