Zulip Chat Archive
Stream: general
Topic: Inline rewriting of natural number symbols
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?
Simon Hudon (Mar 31 2020 at 18:56):
you can use change 2 = _
Reid Barton (Mar 31 2020 at 18:56):
rw (show nat.succ (nat.succ 0) = 2, by rfl)
Gabriel Ebner (Mar 31 2020 at 18:59):
@Reid Barton Shouldn't that be ... from rfl?
Reid Barton (Mar 31 2020 at 18:59):
or by refl to save one character
Simon Hudon (Mar 31 2020 at 19:10):
or norm_num [nat.succ_eq_add_one]
Andrew Helwer (Mar 31 2020 at 21:12):
What does show do? Is for inline theorems?
Reid Barton (Mar 31 2020 at 21:21):
show t, from e is an expression of type t, equal to e
Last updated: Dec 20 2023 at 11:08 UTC