mathlib documentation

tactic.rewrite

meta def tactic.match_fn (fn a : expr) :

tactic (expr × expr)

meta def tactic.fill_args (a : expr) :

tactic (expr × list expr)

meta def tactic.mk_assoc_pattern' (fn a : expr) :

tactic (dlist expr)

meta def tactic.mk_assoc_pattern (fn e : expr) :

tactic (list expr)

meta def tactic.mk_assoc (fn : expr) (a : list expr) :

meta def tactic.chain_eq_trans (a : list expr) :

meta def tactic.unify_prefix (a a_1 : list expr) :

meta def tactic.match_assoc_pattern' (p a : list expr) :

tactic (list expr × list expr)

meta def tactic.match_assoc_pattern (fn p e : expr) :

tactic (list expr × list expr)

meta def tactic.mk_eq_proof (fn : expr) (e₀ e₁ : list expr) (p : expr) :

tactic (expr × expr × expr)

meta def tactic.assoc_root (fn assoc a : expr) :

tactic (expr × expr)

meta def tactic.assoc_refl' (fn assoc a a_1 : expr) :

meta def tactic.assoc_refl (fn : expr) :

meta def tactic.flatten (fn assoc e : expr) :

tactic (expr × expr)

meta def tactic.assoc_rewrite_intl (assoc h e : expr) :

tactic (expr × expr)

meta def tactic.enum_assoc_subexpr' (fn a : expr) :

tactic (dlist expr)

meta def tactic.enum_assoc_subexpr (fn e : expr) :

tactic (list expr)

meta def tactic.mk_assoc_instance (fn : expr) :

meta def tactic.assoc_rewrite (h e : expr) (opt_assoc : option expr := none) :

tactic (expr × expr × list expr)

meta def tactic.assoc_rewrite_target (h : expr) (opt_assoc : option expr := none) :

meta def tactic.assoc_rewrite_hyp (h hyp : expr) (opt_assoc : option expr := none) :

meta def tactic.interactive.assoc_rewrite (q : interactive.parse tactic.interactive.rw_rules) (l : interactive.parse interactive.types.location) :

assoc_rewrite [h₀,← h₁] at ⊢ h₂ behaves like rewrite [h₀,← h₁] at ⊢ h₂ with the exception that associativity is used implicitly to make rewriting possible.

meta def tactic.interactive.assoc_rw (q : interactive.parse tactic.interactive.rw_rules) (l : interactive.parse interactive.types.location) :

synonym for assoc_rewrite