>> I'm working on an extension of the locale machinery by a means of >> declaring morphisms for use in locale expressions. Currently morphisms >> only appear within locale expressions. For example, in >> >> interpretation my_locale where A = t and B = s >> >> the parameters A and B of 'my_locale' are mapped to t and s from the >> current context. The extension would introduce a new command >> 'morphism' for declaring morphisms and a new keyword 'under' for >> referring to these morphisms in expressions: >> >> morphism my_morphism where A = t and B = s >> >> interpretation my_locale under my_morphism > > I wonder if "with" could be reused instead?
To my knowledge, »with« is a command and hence cannot be reused as a
keyword. Cf. print_commands.
If the aim is to avoid introducing a new keyword, maybe »morphisms«
could be a choice.
Florian
OpenPGP_signature
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
