*To*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Best practices for introducing domain specific notation*From*: Dominique Unruh <unruh at ut.ee>*Date*: Mon, 6 May 2019 15:50:08 +0300*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.6.1

Hi,

* With locales, I have the following problems: I cannot separate the notation from the logical context. For example, sometimes my definition will not be in any natural way part of a locale. For example, if I introduce a datatype and an operation on it (say, lists, and · for concatenation) then I would not know where to put the notation. Also, as far as I understand, with locales, there is no way to use the notation (like "including" with bundles) locally without actually using the whole logical context of the locale (in particular, if I want to use some notation from a locale in the statement of a lemma by using "(in name)", that lemma will then automatically be in the name space of the locale). * Bundles seem to have more flexibility. I can put a number of syntax elements together and include them as needed. Unfortunately, it seems that bundles are not extensible. For example, assume a theory that introduces a number of concepts throughout the theory (or even several theories). E.g., inner product, norm, closure of sets, Minkowski product, etc. If I want to use bundles, I have the following choices: o I introduce all the definitions at the beginning of the theory (and thus break the logical structure of the presentation) and make a bundle with syntax at the beginning. o I introduce all the definitions where they fit logically, and introduce syntax only at the very end (as one bundle). Then I cannot use the notation within the theories. o I introduce a new bundle each time I introduce new syntax (and end up with a lot of bundles that I can later combine into one bundle). That avoids the above problems, but it means that I pollute the name space with a lot of temporary bundle names. What is the best approach here?

Best wishes, Dominique.

**Follow-Ups**:**Re: [isabelle] Best practices for introducing domain specific notation***From:*Alexander Krauss

- Previous by Date: [isabelle] [Isabelle2019-RC1] Unhelpful error message (and possible regression)
- Next by Date: [isabelle] Deadline extension |CFP ICTAC 2019|| May 19||Hammamet Tunisia
- Previous by Thread: Re: [isabelle] [Isabelle2019-RC1] Unhelpful error message (and possible regression)
- Next by Thread: Re: [isabelle] Best practices for introducing domain specific notation
- Cl-isabelle-users May 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list