Zulip Chat Archive

Stream: general

Topic: show by


view this post on Zulip Kenny Lau (Sep 10 2020 at 17:41):

I just noticed that the by is redundant in show if you have a tactic block:

theorem foo {a b c d : } (hab : a = b) (hcd : c = d) : a + c = b + d :=
show _, { rw hab, rw hcd, }

Last updated: May 15 2021 at 23:13 UTC