> On 8 Jan 2022, at 01:37, Tobias Nipkow <[email protected]> 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. Cheers, Gerwin
signature.asc
Description: Message signed with OpenPGP
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
