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: May 13 2021 at 06:15 UTC