mathlib documentation


meta def old_conv.step {α : Type} :

meta def old_conv.istep {α : Type} :
old_conv αold_conv unit

meta def conv.replace_lhs  :

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.