mathlib documentation

tactic.rewrite

source
meta def tactic.match_fn  :
expr → expr → tactic (expr × expr)

source
meta def tactic.fill_args  :
expr → tactic (expr × list expr)

source
meta def tactic.mk_assoc_pattern'  :
expr → expr → tactic (dlist expr)

source
meta def tactic.mk_assoc_pattern  :
expr → expr → tactic (list expr)

source
meta def tactic.mk_assoc  :
expr → list expr → tactic expr

source
meta def tactic.chain_eq_trans  :
list expr → tactic expr

source
meta def tactic.unify_prefix  :
list expr → list expr → tactic unit

source
meta def tactic.match_assoc_pattern'  :
list expr → list expr → tactic (list expr × list expr)

source
meta def tactic.match_assoc_pattern  :
expr → expr → expr → tactic (list expr × list expr)

source
meta def tactic.mk_eq_proof  :
expr → list expr → list expr → expr → tactic (expr × expr × expr)

source
meta def tactic.assoc_root  :
expr → expr → expr → tactic (expr × expr)

source
meta def tactic.assoc_refl'  :
expr → expr → expr → expr → tactic expr

source
meta def tactic.assoc_refl  :
expr → tactic unit

source
meta def tactic.flatten  :
expr → expr → expr → tactic (expr × expr)

source
meta def tactic.assoc_rewrite_intl  :
expr → expr → expr → tactic (expr × expr)

source
meta def tactic.enum_assoc_subexpr'  :
expr → expr → tactic (dlist expr)

source
meta def tactic.enum_assoc_subexpr  :
expr → expr → tactic (list expr)

source
meta def tactic.mk_assoc_instance  :
expr → tactic expr

source
meta def tactic.assoc_rewrite  :
expr → expr → (option expr := none) → tactic (expr × expr × list expr)

source
meta def tactic.assoc_rewrite_target  :
expr → (option expr := none) → tactic unit

source
meta def tactic.assoc_rewrite_hyp  :
expr → expr → (option expr := none) → tactic expr

source
meta def tactic.interactive.assoc_rewrite  :
interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → tactic unit

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.

source
meta def tactic.interactive.assoc_rw  :
interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → tactic unit

synonym for assoc_rewrite