Re: [isabelle] Strange behavior of binders in locales



It seems that the behavior can be reproduced even without a hierarchy of locales.
The following reproduces the error message:

locale A
begin

definition test:: "('a â bool) â bool" (binder "+" 10)
  where "test P â True"

notation test (binder "-" 10)

end

without locale it doesn't produce any error message.


Best,

Diego

-----UrsprÃngliche Nachricht-----
Von: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] Im Auftrag von Diego Marmsoler
Gesendet: Donnerstag, 17. August 2017 17:37
An: cl-isabelle-users at lists.cam.ac.uk
Betreff: [isabelle] Strange behavior of binders in locales

Dear Isabelle experts,

 

I have the following problem when trying to build a locale and changing the concrete syntax of a binder:

 

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)

 

Many thanks,

 

Diego

 

 

--

Diego Marmsoler

Technische UniversitÃt MÃnchen

FakultÃt fÃr Informatik

Lehrstuhl fÃr Software & Systems Engineering

Zimmer MI 00.11.057

Boltzmannstr. 3

85748 Garching bei MÃnchen

Tel. +49 (0)89 289-17384 

Fax. +49 (0)89 289-17307

 <mailto:diego.marmsoler at tum.de> diego.marmsoler at tum.de

 <http://www4.in.tum.de/~marmsole/> http://www4.in.tum.de/~marmsole/

 

 

Attachment: smime.p7s
Description: S/MIME cryptographic signature



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