# Zulip Chat Archive

## Stream: general

### Topic: decidable_classical linter complaint

#### Paul van Wamelen (Aug 29 2020 at 22:58):

I have a theorem that I would like to add to the ring_theory/unique_factorization_domain.lean file, but the `decidable_classical`

linter complains with

```
The following `decidable` hypotheses should be replaced with
`classical` in the proof. argument 4: [dec : decidable_eq (associates α)]
```

There are many other theorems that have the exact same hypothesis, but without a complaint. Why is that? Also, how do I fix this case?

#### Mario Carneiro (Aug 29 2020 at 23:05):

As long as the hypothesis is referenced directly in the statement (usually invisibly because it is a type class argument), the linter will not complain

#### Mario Carneiro (Aug 29 2020 at 23:05):

You can fix it by removing the decidable_eq instance from the theorem, and then starting the proof with `classical,`

#### Mario Carneiro (Aug 29 2020 at 23:10):

I see in ring_theory/unique_factorization_domain.lean that the `dec`

hypothesis is added on L305, included in the definition `factors`

(meaning that all theorems directly about `factors`

will need this assumption), and later explicitly omitted in theorems `eq_of_prod_eq_prod`

and `prod_le`

, by putting `omit dec`

before the theorem and `include dec`

after. You can do that for your theorem as well

#### Paul van Wamelen (Aug 29 2020 at 23:27):

Thanks Mario, I'll try that!

Last updated: May 14 2021 at 14:20 UTC