Defining notation

Stream: lean4

[Marcus Rossel]

I have a predicate def hasEdgeFromTo (g : Graph κ) (k k' : κ) : Prop := ..., which I would like to wrap in the notation a-g->b.
I tried defining this as:

notation a "-" g "->" b => hasEdgeFromTo g a b

But when I go to use it, I get the error:

failed to synthesize instance
  HSub κ (LGraph κ) ?m.4716

So I guess the subtraction notation is conflicting with my notation here.
What is the correct way to define the edge-notation?

[Kyle Miller]

You could add some more symbols to disambiguate, like a-[g]->b. You might also consider taking advantage of dot notation; renaming hasEdgeFromTo to Graph.adj, you could have g.adj a b.

structure Graph (κ : Type u) where
  adj : κ → κ → Prop

def Graph.is_symmetric (g : Graph κ) : Prop :=
∀ v w, g.adj v w ↔ g.adj w v

notation v " -[" g "]-> " w => Graph.adj g v w

def Graph.is_symmetric' (g : Graph κ) : Prop :=
∀ v w, (v -[g]-> w) ↔ (w -[g]-> v)

@[reducible] def Graph.V (g : Graph κ) := κ

def Graph.adj' {g : Graph κ} (v w : g.V) : Prop := g.adj v w

notation v " →G " w => Graph.adj' v w

def Graph.is_symmetric'' (g : Graph κ) : Prop :=
∀ (v w : g.V), (v →G w) ↔ (w →G v)