Zulip Chat Archive

Stream: general

Topic: obtain rfl


view this post on Zulip Johan Commelin (Aug 09 2019 at 07:11):

I just noticed that we can now replace the pattern

have : x = 0 := foobar baz xyzzy,
subst x -- or `subst this`

with

obtain rfl : x = 0 := foobar baz xyzzy

view this post on Zulip Floris van Doorn (Aug 09 2019 at 15:03):

Yeah, the obtain tactic very nice!

view this post on Zulip Rob Lewis (Aug 09 2019 at 16:21):

Note that if foobar baz xyzzy elaborates without the expected type, this is really just cases foobar baz xyzzy. And even if you use obtain, the rfl shouldn't be necessary.


Last updated: May 13 2021 at 06:15 UTC