Re: [isabelle] Performance considerations of locales

Just a general comment: locales have been around for a long time but we are still figuring out how to use them effectively in large developments. Papers on the locale methodology itself ought to be publishable, certainly at the Isabelle workshop (which we hope to hold next summer at flOC 2022).

On 27 Sep 2021, 09:57 +0100, Norbert Schirmer <nschirmer at>, wrote:

The tradeoff is between simplicity / readability vs. performance. Especially the neat thing about attributes (compared to declarations) is that you can already provide them to almost all relevant functions like definitions, derived specifications (like function package) and ’notes’. Note that we not only use plain definitions with large terms but also derived concepts like (partial) functions which besides the defining equation also result in a bunch of theorems (like induction) with large terms.

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