Zulip Chat Archive

Stream: general

Topic: Inline rewriting of natural number symbols


view this post on Zulip Andrew Helwer (Mar 31 2020 at 18:52):

Is there an easy way to rewrite nat.succ nat.succ 0 into 2 without having to define it in a separate theorem then using that theorem in a rw?

view this post on Zulip Simon Hudon (Mar 31 2020 at 18:56):

you can use change 2 = _

view this post on Zulip Reid Barton (Mar 31 2020 at 18:56):

rw (show nat.succ (nat.succ 0) = 2, by rfl)

view this post on Zulip Gabriel Ebner (Mar 31 2020 at 18:59):

@Reid Barton Shouldn't that be ... from rfl?

view this post on Zulip Reid Barton (Mar 31 2020 at 18:59):

or by refl to save one character

view this post on Zulip Simon Hudon (Mar 31 2020 at 19:10):

or norm_num [nat.succ_eq_add_one]

view this post on Zulip Andrew Helwer (Mar 31 2020 at 21:12):

What does show do? Is for inline theorems?

view this post on Zulip Reid Barton (Mar 31 2020 at 21:21):

show t, from e is an expression of type t, equal to e


Last updated: May 16 2021 at 05:21 UTC