Overlapping four-place notation

Stream: lean4

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Hi! I am trying to introduce a notation which partially overlaps with $\pmod N$ notation from mathlib. It works in one variant, and not in another. Does anybody understand why this is happening?

import Mathlib.Data.Nat.ModEq

#check 1 ≡ 5 [MOD 4] -- 1 ≡ 5 [MOD 4] : Prop

notation:50 x " ≡ " y " [AMOD " N "]" => N
#check 1 ≡ 2 [AMOD 3] -- 3 : ℕ

notation:50 a " ∣ " b " ≡ " c " [BMOD " N "]" => N
#check 1 ∣ 2 ≡ 3 [BMOD 4] -- unexpected token '[BMOD'; expected '[AMOD' or '[MOD'

[Sebastian Ullrich]

You'll probably want to increase the precedence of a so that it doesn't capture all of 1 | 2 as a single term

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I used a Unicode ∣ to avoid clashing with |. Increasing the precedence does not seem to change anything.

[Kyle Miller]

Here's the incantation:

notation:50 a:51 " ∣ " b:51 " ≡ " c " [BMOD " N "]" => N

You have to match the precedences that the infix command sets for the ∣ operator

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Thank you! Are you sure this is about the precedence of the ∣ operator? Using a symbol which is certainly not an infix operator fails in the same way:

notation:50 a " ✨ " b " ≡ " c " [BMOD " N "]" => N
#check 1 ✨ 2 ≡ 3 [BMOD 4] -- unexpected token '[BMOD'; expected '[AMOD' or '[MOD'

but with notation:50 a " ✨ " b:51 " ≡ " c " [BMOD " N "]" => N, it works. So I am led to conclude that without the extra precedence, it is being parsed as 1 ✨ (2 ≡ 3 [BMOD 4]). The ≡ mod notations from mathlib also have precedence 50.

[Sebastian Ullrich]

I think you're right, b's precedence is the one that matters

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Is there anything I could read to better understand the Pratt parsing rules of Lean? This article is nice but it doesn't account for the feature of "output precedences" syntax:$prec that Lean has.

[Sebastian Ullrich]

The new manual is in progress but does this help in the meantime? I wouldn't think about it on the Pratt algorithm level but as a combination of the placeholder and longest parse rules mentioned there

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Ahh, not really. "Local longest parse" isn't precise enough for me to predict or understand what would happen in situations like the one above. I mean, 1 ∣ 2 ≡ 3 [BMOD 4] is a longer parse than 1 ∣ (2 ≡ 3 <error>), I think? But maybe the "local" part implies that once we start parsing the nested b:term and see something that _could_ be 2 ≡ 3 [MOD .., we'll commit to that and hence the error occurs? Overall, a precise description would be preferable (but I understand it's not super high priority to explain the weeds).