generic constraints

Stream: lean4

[J. O.]

I have two parameters which are generic, but they need to both have a ToString instance. is there any way to put a constraint for the generic type, so that the type can only be one that has a ToString instance? thanks in advance

[Mario Carneiro]

example (A : Type) [ToString A] : ...

[J. O.]

that works. thanks! what type of argument is that again. time to look at the manual

[Johan Commelin]

"instance implicit"

[J. O.]

ah yes