## Stream: new members

### Topic: Apply a rewrite on a precise term

#### Hamza Maimoune (Feb 08 2020 at 14:22):

Hello everyone,

I would like to ask you if there is a way to apply a rewrite tactic on a particular term. For example, if I want to replace only the second term of an expression.

Thank you.

#### Ryan Lahfa (Feb 08 2020 at 14:30):

You can perform something like:

conv_rhs {
rw [what you want]
}


It'll rewrite the right hand only.
Inside of a conv block, you can use congr in order to split parts of your equation, like if you have A * B, congr will give you two goals A then B, you can use skip to through some you don't want.

Thank you both

#### Patrick Massot (Feb 08 2020 at 20:30):

@Hamza MAIMOUNE , please also try:

example (a b : ℕ) (h : a = b): a + a + a + a + a = 0 :=
begin
rw [h] {occs := occurrences.pos [1, 3]},
sorry,
end


The syntax is awfully verbose but it can still be quicker than a complicated conv navigation.

Last updated: May 13 2021 at 22:15 UTC