Deriving for `def`

Stream: new members

[Josh Cohen]

Suppose I have an inductive type A that has derived DecidableEq. How can I derive or otherwise easily define instance DecidableEq for def B := A?

[Joël Riou]

Under your assumptions, inferInstanceAs (DecidableEq A) is a term of type DecidableEq B.

[Josh Cohen]

Thanks!

[Kyle Miller]

def B := A
deriving DecidableEq