dif_pos

Stream: general

[Reid Barton]

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

[Simon Hudon]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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.

[Simon Hudon]

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

[Reid Barton]

Just tested and it does solve my (former) problem