Zulip Chat Archive

Stream: general

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


view this post on Zulip Kevin Buzzard (Apr 25 2020 at 16:26):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 16:27):

rw sometimes also unfolds recursively defined functions on inductive types

view this post on Zulip Kenny Lau (Apr 25 2020 at 16:27):

with constructor


Last updated: May 10 2021 at 17:39 UTC