Lower operator priority

Stream: lean4

[Martin Dvořák]

I defined an infix operator for Insert.insert and I would like it to have lower priority than { } for repeated inserts into a singleton.

import Mathlib

infixr:66 (priority := 1) " ᕃ " => Insert.insert

example (x y z : ℚ) (s : Set ℚ) (hs : s = {y, z}) : x ᕃ s = {x, y, z} := by
  sorry

Currently the goal is displayed as:

x ᕃ s = x ᕃ y ᕃ {z}

I want the goal to be displayed as:

x ᕃ s = {x, y, z}

What can I do?
I'm not sure whether priority is for that.

[Eric Wieser]

It sounds like you're talking about delaborator priority, not notation parsing priority

[Eric Wieser]

I don't know if the former notion exists

[Martin Dvořák]

Can it be worked around using app_unexpander or something?

[Eric Wieser]

Yes, you can use syntax instead of notation, and then write your own delaborator manually