algebra.expr - mathlib3 docs

Helpers to invoke functions involving algebra at tactic time #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

It's not clear whether using instance_cache is a sensible choice here. In particular, we need to use these tactics below when the algebraic instances are local variables that aren't in the "real" instance cache (the one used by tactic.reset_instance_cache).

source

meta def expr.has_one (t : tactic.instance_cache) :

tactic (tactic.instance_cache × has_one expr)

Produce a has_one instance for the type cached by t, such that 1 : expr is the one of that type.

source

meta def expr.has_zero (t : tactic.instance_cache) :

tactic (tactic.instance_cache × has_zero expr)

Produce a has_zero instance for the type cached by t, such that 0 : expr is the zero of that type.

source

meta def expr.has_mul (t : tactic.instance_cache) :

tactic (tactic.instance_cache × has_mul expr)

Produce a has_mul instance for the type cached by t, such that (*) : expr → expr → expr is the multiplication of that type.

source

meta def expr.has_add (t : tactic.instance_cache) :

tactic (tactic.instance_cache × has_add expr)

Produce a has_add instance for the type cached by t, such that (+) : expr → expr → expr is the addition of that type.