[isabelle-dev] Locale morphisms

[Florian Haftmann]

>> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220108/fb785568/attachment.sig>