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, ininterpretation my_locale where A = t and B = sthe 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? Tobias
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 syntax.Clemens _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
