delta_instance id₁ id₂ ... tries to solve the goal by calling apply_instance,
first unfolding the definitions in idᵢ.
Tries to derive instances by unfolding the newly introduced type and applying type class resolution.
For example,
@[derive ring] def new_int : Type := ℤ
adds an instance ring new_int, defined to be the instance of ring ℤ found by apply_instance.
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 defs.