mathlib3 documentation

core / init.meta.converter.conv

meta def conv (α : Type u) :

conv α is a tactic for discharging goals of the form lhs ~ rhs for some relation ~ (usually equality) and fixed lhs, rhs. Known in the literature as a conversion tactic. So for example, if one had the lemma p : x = y, then the conversion for p would be one that solves p.

Instances for conv
@[protected, instance]
meta def conv.monad  :
@[protected, instance]
@[protected, instance]
meta def conv.convert (c : conv unit) (lhs : expr) (rel : name := name.mk_string "eq" name.anonymous) :

Applies the conversion c. Returns (rhs,p) where p : r lhs rhs. Throws away the return value of c.

meta def conv.lhs  :
meta def conv.rhs  :
meta def conv.update_lhs (new_lhs h : expr) :

⊢ lhs = rhs ~~> ⊢ lhs' = rhs using h : lhs = lhs'.

meta def conv.change (new_lhs : expr) :

Change lhs to something definitionally equal to it.

meta def conv.skip  :

Use reflexivity to prove.

meta def conv.whnf  :

Put LHS in WHNF.

meta def conv.congr  :

Take the target equality f x y = X and try to apply the congruence lemma for f to it (namely x = x' → y = y' → f x y = f x' y').

meta def conv.funext  :

Create a conversion from the function extensionality tactic.