mathlib documentation


meta def old_conv.step {α : Type} (c : old_conv α) :
meta def old_conv.istep {α : Type} (line0 col0 line col : ) (c : old_conv α) :
meta def conv.replace_lhs (tac : exprtactic (expr × expr)) :

The conv tactic provides a conv within a conv. It allows the user to return to a previous state of the outer conv block to continue editing an expression without having to start a new conv block.

guard_target t fails if the target of the conv goal is not t. We use this tactic for writing tests.