[isabelle-dev] Towards localized syntax: bundle mixins for locale and class specifications – Discussion of alternatives
florian.haftmann at informatik.tu-muenchen.de
Sun Nov 1 18:09:32 CET 2020
currently the syntax for bundle mixins for locale / class specifications
looks as follows:
locale / class foo = import +
While this use of »includes« rests firmly on established traditions, it
is a little bit unsatisfactory since it also applies to the »import«
expression, but is notated *after* it.
I had thought about something like
locale foo = import +
instead but this would require an artificial construction identifying
nested contexts as »morally being global« internally.
A more inspiring solution could be to abandon the existing »includes«
syntax entirely and replace it by a specific toplevel construct, e.g.
including bundles lemma foo: ‹…› if ‹…› for …
including bundles context group
including bundles locale bar = …
This looks charming but the progressive participle is reserved for
proofs. For the same reason »with« won't do.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 228 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev