Zulip Chat Archive
Stream: general
Topic: decidable & classical
Yury G. Kudryashov (Apr 09 2020 at 00:24):
Do we have a standard way to deal with different instances of decidable?
Yury G. Kudryashov (Apr 09 2020 at 00:25):
I can congr; split_ifs; refl but it's not convenient.
Yury G. Kudryashov (Apr 09 2020 at 00:26):
Note that this problem is present even with open_locale classical because some lemmas generate instances based on classical.
Yury G. Kudryashov (Apr 09 2020 at 00:28):
E.g., when I do rw inside the argument of ite.
Yury G. Kudryashov (Apr 09 2020 at 00:30):
Not rw but simp only.
Simon Hudon (Apr 09 2020 at 00:31):
Why do you have access to multiple equivalent instances of decidable? I think eliminating the redundancy would be best if it's possible
Yury G. Kudryashov (Apr 09 2020 at 00:54):
It seems that this will be fixed in 3.8.0.
Yury G. Kudryashov (Apr 09 2020 at 00:55):
I mean, my particular source of redundancy.
Simon Hudon (Apr 09 2020 at 00:55):
What's the fix?
Yury G. Kudryashov (Apr 09 2020 at 00:55):
It came from simplifying condition of ite, and before 3.8.0 the congr lemma inserts some eq.rec.
Yury G. Kudryashov (Apr 09 2020 at 01:01):
Last updated: Dec 20 2023 at 11:08 UTC