[isabelle-dev] Locale morphisms
nipkow at in.tum.de
Fri Jan 7 15:37:42 CET 2022
On 07/01/2022 15:12, Clemens Ballarin wrote:
> Dear Isabelle Developers,
> 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
> morphism my_morphism where A = t and B = s
> interpretation my_locale under my_morphism
I wonder if "with" could be reused instead?
> This will be helpful especially in applications where locales have more than
> just a handful of parameters.
> I'm mainly writing to find out whether the new keywords 'morphism' and 'under'
> would be considered appropriate in the current framework of Isabelle's outer
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5535 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev