Tries to derive instances by unfolding the newly introduced type and applying type class resolution.
@[derive ring] def new_int : Type := ℤ
Multiple instances can be added with
@[derive [ring, module ℝ]].
This derive handler applies only to declarations made using
def, and will fail on such a
declaration if it is unable to derive an instance. It is run with higher priority than the built-in
handlers, which will fail on