mathlib documentation

core / init.meta.rewrite_tactic

source
def tactic.id_tag.rw  :
unit
Equations
source
structure tactic.rewrite_cfg  :
Type

Configuration options for the rewrite tactic.

source
meta constant tactic.rewrite_core (h e : expr) (cfg : tactic.rewrite_cfg := {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}, symm := ff, occs := occurrences.all}) :
tactic (expr × expr × list expr)

Rewrite the expression e using h. The unification is performed using the transparency mode in cfg. If cfg.approx is tt, then fallback to first-order unification, and approximate context during unification. cfg.new_goals specifies which unassigned metavariables become new goals, and their order. If cfg.instances is tt, then use type class resolution to instantiate unassigned meta-variables. The fields cfg.auto_param and cfg.opt_param are ignored by this tactic (See tactic.rewrite). It a triple (new_e, prf, metas) where prf : e = new_e, and metas is a list of all introduced meta variables, even the assigned ones.

TODO(Leo): improve documentation and explain symm/occs

source
meta def tactic.rewrite (h e : expr) (cfg : tactic.rewrite_cfg := {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}, symm := ff, occs := occurrences.all}) :
tactic (expr × expr × list expr)
source
meta def tactic.rewrite_target (h : expr) (cfg : tactic.rewrite_cfg := {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}, symm := ff, occs := occurrences.all}) :
tactic unit
source
meta def tactic.rewrite_hyp (h hyp : expr) (cfg : tactic.rewrite_cfg := {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}, symm := ff, occs := occurrences.all}) :
tactic expr