infix notation precedence

Stream: general

[Sean Leather]

I want something that is effectively equivalent to this:

reserve infix ` d∉ `:51
local notation a d∉ l := blah l a

However, I'm guessing it's not a good idea to use reserve here. I've tried several notation declarations (e.g. notation a ` d∉ `:51 l and notation a ` d∉ `:51 l:0), but I can't seem to get the precedence right. What's the correct way to specify the above without using reserve?

[Sebastian Ullrich]

Why are you not using local infix?

[Sean Leather]

Because then I would have to write:

local infix ` d∉ `:51 := λ a l, blah l a

[Sebastian Ullrich]

I see. The equivalent to infix should be

a ` d∉ `:51 l:51

[Sean Leather]

Ah ha! Can you help me understand that?

[Sebastian Ullrich]

The first :51 sets the token's binding power, whereas the second one sets the right-binding power (rbp) the Pratt parser will use while parsing that expression. The parser will try to parse an expression until it encounters a token with bp <= its rbp. The rbp used initially is 0.
For example, on the input a d∉ b d∉ c (not that it makes much sense in your case), the parser will start with rbp 0, read the leading term a, read the token with bp > 0, then recurse for the notation RHS using rbp 51. This recursive call will read the leading b, then stop at the token since 51 <= 51, and return. The original parser call will accept it, since it uses rbp 0, and complete parsing the input. Thus the output is (a d∉ b) d∉ c because the parser for the first notation's RHS stopped after b.

[Sebastian Ullrich]

If you use infixr instead and do #print d∉, you'll see that the RHS now has rbp 50 so that it will consume the d∉ token

[Sean Leather]

Thanks, @Sebastian Ullrich!