(static) multimethods in Lean

Stream: lean4

[Yuri de Wit]

I recently got to know that Julia supports multi-methods (multi dispatch as opposed to a single dispatch common in OO languages) and it is used as a cleaner, more powerful way to solve the expression problem. Julia does this at runtime, although other than development I wouldnt want/need that in production.

Could the same be achieved statically in Lean4 with multi-parameter type classes?

[Anne Baanen]

Definitely! For example, mathlib has a "scalar multiplication" operator docs#has_scalar.smul that dispatches on the left and right side of the multiplication simultaneously.