example overloading notation

Stream: general

[Kind Bubble]

I have several situations where I'd like to use the same unicode symbol for multiple purposes. I want Lean to try to match one usage and try the other only if the first one fails.

Probably the most important one uses the cross product symbol. But it doesn't matter. Behold my favorite symbol of the elephant:

𓃰

Here's an example I want to work:

variable {A : Type}
variable {a : A}
variable {B : Type}
variable {g : B -> Nat}

notation F "𓃰" => F + g F
notation F "𓃰" => F a

These are pretty separate and I would imagine there is some feature which can manage the ambiguity. How might I make this example work?

[Trebor Huang]

You can use a typeclass Elephant with an operation elephantize. The notation unfolds to the elephantize operation, and you give two different typeclass instances with F + g F and F a.