a + succ b syntactically succ(a+b)?

Stream: general

[Kevin Buzzard]

Of course not.

So why does this work:

structure foo (n : ℕ).

open nat

theorem foo_succ (n : ℕ) : foo (succ n) = foo n := sorry

example (a b : ℕ) : foo (a + succ b) = foo (a + b) :=
begin
  rw foo_succ, -- ??
end

[Kenny Lau]

rw sometimes also unfolds recursively defined functions on inductive types

[Kenny Lau]

with constructor