Zulip Chat Archive

Stream: general

Topic: decidable & classical


view this post on Zulip Yury G. Kudryashov (Apr 09 2020 at 00:24):

Do we have a standard way to deal with different instances of decidable?

view this post on Zulip Yury G. Kudryashov (Apr 09 2020 at 00:25):

I can congr; split_ifs; refl but it's not convenient.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Apr 09 2020 at 00:28):

E.g., when I do rw inside the argument of ite.

view this post on Zulip Yury G. Kudryashov (Apr 09 2020 at 00:30):

Not rw but simp only.

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Apr 09 2020 at 00:54):

It seems that this will be fixed in 3.8.0.

view this post on Zulip Yury G. Kudryashov (Apr 09 2020 at 00:55):

I mean, my particular source of redundancy.

view this post on Zulip Simon Hudon (Apr 09 2020 at 00:55):

What's the fix?

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Apr 09 2020 at 01:01):

lean#159


Last updated: May 14 2021 at 04:22 UTC