mathlib3 documentation

tactic.delta_instance

meta def tactic.delta_instance (ids : list name) :

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ᵢ.

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 defs.