mathlib documentation


meta def conv  :
Type uType 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.

meta def conv.monad  :



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  :
exprexprconv unit

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

meta def conv.change  :

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.