Defining notation with two arguments separated by space

Stream: lean4

[Adrian Wüthrich]

I'm having some trouble defining a custom notation for Finset.card (Rel.interedges (SimpleGraph.Adj G) s sᶜ), where G is a simple graph and s is a finset. I'd like to denote this by |∂ G s| .
Here is my attempt:

import Mathlib.Combinatorics.SimpleGraph.Density

variable {V : Type*} [DecidableEq V] [Fintype V]
variable (G : SimpleGraph V) [DecidableRel G.Adj]
variable (s : Finset V)

notation:max "|∂" G:100 "  " s:100 "|" => Finset.card (Rel.interedges (SimpleGraph.Adj G) s sᶜ) -- error here

-- error message: invalid parser '«term|∂__|»', invalid empty symbol

What does work is the notation `notation:max "|∂" G:100 "×" s:100 "|" => Finset.card (Rel.interedges (SimpleGraph.Adj G) s sᶜ). This also works for symbols other than ×, but I'd prefer having a blank space.

[Eric Wieser]

Can you just drop the " " bit entirely?

[Adrian Wüthrich]

then the definition of the notation works but when i try #check |∂ G s|, the s is underlined and I get the message "expected no space before".

[Eric Wieser]

This works for me:

notation:max "|∂" G:arg s:arg "|" => Finset.card (Rel.interedges (SimpleGraph.Adj G) s sᶜ

[Adrian Wüthrich]

Thank you so much! I did not know about the precedence arg and was trying to get some random numbers to work.