As usual, sorry, if this is a double up, but I did search through the list for related posts without success.
I have been a bit frustrated recently by phantom locale notations making my proof states impossible to read.
It seems to come up in locale hierarchies where the notation for abbreviations is changed to reflect strengthened defining properties.
This is a simple example:
locale pos =
x :: int
x_pos: ‹0 ≤ x›
‹half ≡ x div 2›
locale big = pos +
x_big: ‹10 ≤ x›
locale pos_big =
Y: pos y
term "half" ―‹result: "♣"›
It seems that the locale _expression_ is including the pos notation for half (rather than Y.half) and it is overriding the big notation for half!
If I reverse the order of inclusion this changes.
locale big_pos =
Y: pos y +
term "half" ―‹result: "♠"›
This is often a viable a work around, but not always. For example if I have a local interpretation in the locale the same phenomena occurs.
I am tempted to see this as a bug, rather than a feature.
Anyone else had this problem? Work arounds?