mathlib3 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.

Instances for tactic.rewrite_cfg
source
meta constant tactic.rewrite_core (h e : expr) (cfg : tactic.rewrite_cfg := {to_apply_cfg := {md := tactic.transparency.reducible, approx := bool.tt, new_goals := tactic.new_goals.non_dep_first, instances := bool.tt, auto_param := bool.tt, opt_param := bool.tt, unify := bool.tt}, symm := bool.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 := tactic.transparency.reducible, approx := bool.tt, new_goals := tactic.new_goals.non_dep_first, instances := bool.tt, auto_param := bool.tt, opt_param := bool.tt, unify := bool.tt}, symm := bool.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 := tactic.transparency.reducible, approx := bool.tt, new_goals := tactic.new_goals.non_dep_first, instances := bool.tt, auto_param := bool.tt, opt_param := bool.tt, unify := bool.tt}, symm := bool.ff, occs := occurrences.all}) :
tactic unit
source
meta def tactic.rewrite_hyp (h hyp : expr) (cfg : tactic.rewrite_cfg := {to_apply_cfg := {md := tactic.transparency.reducible, approx := bool.tt, new_goals := tactic.new_goals.non_dep_first, instances := bool.tt, auto_param := bool.tt, opt_param := bool.tt, unify := bool.tt}, symm := bool.ff, occs := occurrences.all}) :
tactic expr