Alias for many instance implicits

Stream: lean4

[Alex Sweeney]

I have a few functions with 4 instance implicits because I do arithemtic on α. Is there a shorthand for this? I tried creating a new class AddSubMulDiv but I can't figure out how to make it inherit or alias the 4 classes.

def step [Add α] [Sub α] [Mul α] [Div α] (...) where ...

[Kevin Buzzard]

extend them and it should work fine.

[Sebastian Ullrich]

docs4#Lean.Parser.Command.classAbbrev registers instances in both directions