tactic.nth_rewrite.basic

source

meta structure tactic.nth_rewrite.cfg :

Type

to_rewrite_cfg : tactic.rewrite_cfg
try_simp : bool
discharger : tactic unit
simplifier : expr → tactic (expr × expr)

Configuration options for nth_rewrite.

source

meta structure tactic.nth_rewrite.tracked_rewrite :

Type

exp : expr
proof : tactic expr
addr : option (list expr_lens.dir)

A data structure to track rewrites of subexpressions. The field exp contains the new expression, while proof contains a proof that exp is equivalent to the expression that was rewritten.

source

meta def tactic.nth_rewrite.tracked_rewrite.eval (rw : tactic.nth_rewrite.tracked_rewrite) :

tactic (expr × expr)

Postprocess a tracked rewrite into a pair of a rewritten expression and a proof witness of the rewrite.