# mathlibdocumentation

tactic.delta_instance

meta def tactic.delta_instance  :

delta_instance ids tries to solve the goal by calling apply_instance, first unfolding the definitions in ids.

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.