Zulip Chat Archive

Stream: general

Topic: obtain rfl


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

Floris van Doorn (Aug 09 2019 at 15:03):

Yeah, the obtain tactic very nice!

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: Dec 20 2023 at 11:08 UTC