[isabelle] Questions on locales - structure keyword and local definitions
- To: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>
- Subject: [isabelle] Questions on locales - structure keyword and local definitions
- From: "C.L. Edmonds" <cle47 at cam.ac.uk>
- Date: Tue, 6 Oct 2020 12:05:41 +0000
- Accept-language: en-GB, en-US
- Authentication-results: lists.cam.ac.uk; dkim=none (message not signed) header.d=none; lists.cam.ac.uk; dmarc=none action=none header.from=cam.ac.uk;
- Thread-index: AQHWm9RLQ+FdAzylF02484j74GhISg==
- Thread-topic: Questions on locales - structure keyword and local definitions
I've been doing a bit of work with locales lately, something I haven't had much past experience in. Would be interested in hearing any thoughts on the following questions.
- When should the (structure) keyword be used for a locale parameter, and what effect does it have?
- Are there any advantages/disadvantages to defining a type outside of the locale (and related methods), vs just using locale parameters and local definitions? To give an example. Say I have a structure which is defined by two different sets. Based on what I've found, one common option appears to be defining a new record type outside of the locale to represent the structure, which would later be used for a locale parameter. I can then define a number of functions/definitions using this type globally, however some (if not all) of these definitions make more sense conditionally (i.e, within a locale with certain assms). The other option appears to be representing these sets as parameters of the locale and defining all operations locally. I've seen both done in the examples I've looked at and would be interested in hearing thoughts either way.
This archive was generated by a fusion of
Pipermail (Mailman edition) and