[isabelle-dev] Locale morphisms
kleing at unsw.edu.au
Fri Jan 7 23:28:28 CET 2022
> On 8 Jan 2022, at 01:37, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 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 expressions:
>> morphism my_morphism where A = t and B = s
>> interpretation my_locale under my_morphism
> I wonder if "with" could be reused instead?
I'd second that.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 833 bytes
Desc: Message signed with OpenPGP
More information about the isabelle-dev