1.11. Conv mode

🔗tactic
conv

conv => ... allows the user to perform targeted rewriting on a goal or hypothesis, by focusing on particular subexpressions.

See https://lean-lang.org/theorem_proving_in_lean4/conv.html for more details.

Basic forms:

  • conv => cs will rewrite the goal with conv tactics cs.

  • conv at h => cs will rewrite hypothesis h.

  • conv in pat => cs will rewrite the first subexpression matching pat (see pattern).

TODO: a lot of tactics have a conv-equivalent. Add them here. Meanwhile, try other tactics and see which work in conv mode.