Zulip Chat Archive

Stream: general

Topic: example overloading notation

Kind Bubble (Jan 19 2023 at 04:25):

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 (Jan 19 2023 at 04:46):

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.

Last updated: Dec 20 2023 at 11:08 UTC