mathlib3 documentation

core / init.meta.converter.conv

def tactic.id_tag.conv :

Equations

tactic.id_tag.conv = unit.star()

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]

meta def conv.monad_fail :

monad_fail conv

@[protected, instance]

meta def conv.alternative :

alternative conv

meta def conv.convert (c : conv unit) (lhs : expr) (rel : name := name.mk_string "eq" name.anonymous) :

tactic (expr × expr)

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.dsimp (s : option simp_lemmas := option.none) (u : list name := list.nil) (cfg : tactic.dsimp_config := {md := tactic.transparency.reducible, max_steps := simp.default_max_steps, canonize_instances := bool.tt, single_pass := bool.ff, fail_if_unchanged := bool.tt, eta := bool.tt, zeta := bool.tt, beta := bool.tt, proj := bool.tt, iota := bool.tt, unfold_reducible := bool.ff, memoize := bool.tt}) :

dsimp the LHS.

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.