Zulip Chat Archive

Stream: general

Topic: dif_pos


view this post on Zulip Reid Barton (Sep 14 2020 at 00:21):

Shouldn't dif_pos and related functions use {} binders for the decidable argument?

view this post on Zulip Simon Hudon (Sep 14 2020 at 00:28):

You mean the lemmas? I think that might be an improvement

view this post on Zulip Reid Barton (Sep 14 2020 at 00:33):

Yeah, I just ran into a case (that still I don't really understand) where by_cases h : ... followed by rw dif_pos h didn't work, but it did work once I added open_locale classical

view this post on Zulip Reid Barton (Sep 14 2020 at 00:33):

The proposition I was casing on definitely doesn't have a decidable instance

view this post on Zulip Reid Barton (Sep 14 2020 at 00:34):

So I'm confused how I could have been ending up with two different instances. However, since the main purpose of dif_pos is to eliminate a dite application, it would make sense to just use the instance contained in that application.

view this post on Zulip Simon Hudon (Sep 14 2020 at 00:36):

What happens if you write a version of dif_pos with the right bracketing?

view this post on Zulip Reid Barton (Sep 14 2020 at 00:38):

Just tested and it does solve my (former) problem


Last updated: May 12 2021 at 23:13 UTC