# mathlibdocumentation

tactic.nth_rewrite.basic

meta structure tactic.nth_rewrite.cfg  :
Type

Configuration options for nth_rewrite.

meta structure tactic.nth_rewrite.tracked_rewrite  :
Type
• exp : expr
• proof :
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.