Notation and context

Stream: general

[Kind Bubble]

I have a situation where I want to use the • and ∘ for many different purposes. How might I set these up as notation - a notation which should only apply in some contexts and not others? Are there some more advanced notational options?

For instance, here's some notation:

notation g "•" f => fun (x : X) => g f x

But suppose I only want it to apply when lean can {find} X Y and Z such that f : X -> Y and g : Y -> Z.

[Kind Bubble]

Kind Bubble said:

I have a situation where I want to use the • and ∘ for many different purposes. How might I set these up as notation - a notation which should only apply in some contexts and not others? Are there some more advanced notational options?

For instance, here's some notation:

notation g "•" f => fun (x : X) => g f x

But suppose I only want it to apply when lean can {find} X Y and Z such that f : X -> Y and g : Y -> Z.

I guess this is called "overloaded" and is not allowed.

[Niels Voss]

I think this is normally accomplished using typeclasses, which have functionality that works similar to Interfaces in languages like Java and C#.

[Niels Voss]

For example in Lean 3, there's a typeclass called has_add (in Lean 4 it's just Add). 1 + 2 translates to has_add.add 1 2 I think.