coe_to_fun notation

Stream: general

[orlando]

Hello,
I have two instance of has_coe_to_fun and I would like to differentiate them with 2 differente notations. Is it possible to do that ? Can i extend the class has_coe_to_fun or something like that ?

[Yury G. Kudryashov]

Why do you want two instances? You can use something like @coe_fn _ inst in a notation.