Zulip Chat Archive

Stream: Is there code for X?

Topic: nat.rec_succ


view this post on Zulip Eric Wieser (Sep 10 2020 at 14:05):

Is this builtin to mathlib or lean somewhere?

lemma rec_succ {C:   Type} {zero_f : C 0} {succ_f : Π n, C n  C n.succ} {n : } :
  @nat.rec C zero_f succ_f (n + 1) = succ_f n (@nat.rec C zero_f succ_f n) := rfl

In general, it seems like if I have an inductive rec operating on a object of a known constuctor, I should be able to unfold it one level.

view this post on Zulip Eric Wieser (Sep 10 2020 at 14:06):

( I needed this for a proof about a deliberately awkward def in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/recursive.20let.20in/near/209644962)

view this post on Zulip Reid Barton (Sep 10 2020 at 14:11):

This is the L rule for some Greek letter L

view this post on Zulip Reid Barton (Sep 10 2020 at 14:12):

dsimp should apply it for example

view this post on Zulip Eric Wieser (Sep 10 2020 at 14:21):

Ahh, there's a hidden nat.add_one that I also needed


Last updated: May 07 2021 at 21:10 UTC