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

[Florian Haftmann]

Since this thread did not stimulate any activity I will go on to
document the syntax in NEWS entries and manuals.

Cheers,
	Florian

Am 01.11.20 um 18:09 schrieb 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
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 

-------------- 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/20201121/0e200fb2/attachment.sig>