Re: [isabelle] Proof of concept: BNF-based records

On 16/02/18 15:06, Peter Lammich wrote:
>> One important aspect of localizing the record package is actually the
>> concrete syntax. When that is done properly, syntax could be attached
>> to
>> different term constructions, independently of the underlying record
>> representation.
> Is there a way to do advanced syntax (e.g. nonterminal, syntax,
> translations, parse_translation, print_ast_translation) properly (e.g.
> localized)?

Yes, one merely needs to connect local entities with global items in the
background theory (the so-called foundation), according to the usual
policies of local_theory contexts.

Here the foundation consists of raw syntax and translations, and the
connection might require further tricks that have not been used before.

The whole localization business is about such tricks -- to make things
possible that look impossible at first sight.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.