[isabelle-dev] Towards localized syntax: bundle mixins for locale and class specifications – Discussion of alternatives

[Florian Haftmann]

Dear all,

currently the syntax for bundle mixins for locale / class specifications
looks as follows:

  locale / class foo = import +
    includes bundles
    fixes …
    assumes …
  begin

  …

  end

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

  context
    includes bundles
  begin

  locale foo = import +
    fixes …
    assumes …
  begin

  …

  end

  end

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
  begin

  …

  end

  including bundles locale bar = …

This looks charming but the progressive participle is reserved for
proofs.  For the same reason »with« won't do.

Cheers,
	Florian

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