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`
obtain rfl : x = 0 := foobar baz xyzzy
Floris van Doorn (Aug 09 2019 at 15:03):
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
rfl shouldn't be necessary.
Last updated: May 13 2021 at 06:15 UTC