mathlib documentation


meta structure tactic.nth_rewrite.cfg  :

Configuration options for nth_rewrite.

meta structure tactic.nth_rewrite.tracked_rewrite  :

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.

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