[isabelle-dev] Locale morphisms
florian.haftmann at informatik.tu-muenchen.de
Sat Jan 8 18:37:23 CET 2022
>> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 228 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev