overload `\[[ \]]`

Stream: new members

[Cody Roux]

How can I declare a notation that rebinds the \[[ \]] syntax? It seems that declaring a notation at level 50 does not suffice, any subsequent uses are still parsed as members of some quotient.

[Eric Wieser]

What do you mean by "at level 50"?

[Eric Wieser]

It sounds like you might be confusing priority with precedence

[Cody Roux]

maybe! I just did notation:50 "⟦" φ "⟧" => some_def, and cannot seem to use my notation.

[Eric Wieser]

Yes, that's precedence not priority

[Eric Wieser]

(priority := 2000) is how you specify the latter

[Kevin Buzzard]

Another option is just to use different brackets, unicode has a gazillion

[Kyle Miller]

or notation (priority := high) "⟦" φ "⟧" => some_def rather than specifying a number for the priority.

Precedence is used to disambiguate overlapping parses, by having it so that notations can say "only allow something that parses with precedence level >= N in this position".

[Cody Roux]

@Kevin Buzzard Fair point, though this is the standard notation for what I am trying to define (and as a computer scientist, I feel like there are a couple missing).

[Cody Roux]

Thanks all