delta_instance id₁ id₂ ...
tries to solve the goal by calling apply_instance
,
first unfolding the definitions in idᵢ
.
Guess a name for an instance from its expression.
This is a poor-man's version of the C++ heuristic_inst_name
, and tries much less hard to pick a
good name.
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 def
s.