## 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.

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):

lean#159

Last updated: May 14 2021 at 04:22 UTC