## Stream: general

### Topic: rewrite error: "failed"

#### Kenny Lau (May 13 2020 at 20:55):

example (x y z : ℕ) : x * (y + z) = x * y + x * z :=

/-
failed
state:
x y z : ℕ
⊢ x * (y + z) = x * y + x * z
-/

example (x y z : ℕ) : x * (y + z) = x * y + x * z :=
by rw nat.pow_two

/-
rewrite tactic failed, did not find instance of the pattern in the target expression
?m_1 ^ 2
state:
x y z : ℕ
⊢ x * (y + z) = x * y + x * z
-/


#### Kenny Lau (May 13 2020 at 20:55):

could we modify rw to make the error more precise in the first case?

Last updated: May 10 2021 at 23:11 UTC