*To*: Diego Marmsoler <diego.marmsoler at tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Strange behavior of binders in locales*From*: Makarius <makarius at sketis.net>*Date*: Sat, 19 Aug 2017 20:35:37 +0200*In-reply-to*: <13239d9d0537410db16043ca52926533@tum.de>*References*: <13239d9d0537410db16043ca52926533@tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.1.1

On 17/08/17 17:36, Diego Marmsoler wrote: > > Letâs say I have the following definition within locale A: > > definition myBinder :: "('a â bool) â bool" (binder "Ab" 10) > > where "myBinder P â True" > > Now lets say I have another locale B which is based on A and for which I want to change the syntax of myBinder. > > Therefore I add the following in B: > > notation myBinder (binder "Bb" 10) > > > now I get the following error message: âMore than one parse translation for "\<^const>MyTheory.A.myBinder_binderâ > > > Does someone know how to change the syntax of a binder within a locale? > > (By the way it works well for any other mixfix notation) The binder notation consists of some special tricks on top of syntax translations. The example above shows that local changes of binder syntax has never been used before. Such corner cases may or may not work and it is apriori unclear if that is strange or normal. Isabelle is so complex that it is possible to fall off the "inhabitable area" occasionally. Anyway, a quick test shows that it is possible to remove the old binder explicitly with 'no_notation' and then add the new one, e.g. like this: context begin definition test:: "('a â bool) â bool" where "test P â True" notation test (binder "+" 10) no_notation test (binder "+" 10) notation test (binder "-" 10) end A few more notes: * Definitions in Isabelle/HOL are usually expressed with the equality of HOL (=), not the one of Pure (â). The latter is used internally for foundational purposes, although some users have the habit to abuse it for HOL definitions, because they like the syntactic priority better. Note that for expressions of type bool, it is also possible to use the notation â which has lower syntactic priority (but for binders parentheses are required nonetheless). * Camel case is normally not used in Isabelle sources: there is a general quest for readability of specifications and proofs and camelCaseIsSimplyNotReadable. Makarius

**References**:**[isabelle] Strange behavior of binders in locales***From:*Diego Marmsoler

- Previous by Date: [isabelle] Isabelle2017-RC0: encoding in Isabelle/jEdit
- Next by Date: [isabelle] New AFP entry: The ÎÎ-calculus
- Previous by Thread: Re: [isabelle] Strange behavior of binders in locales
- Next by Thread: [isabelle] clarsimp_all? explode_conj?
- Cl-isabelle-users August 2017 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