Zulip Chat Archive

Stream: general

Topic: decidable_classical linter complaint


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

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

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

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

view this post on Zulip Paul van Wamelen (Aug 29 2020 at 23:27):

Thanks Mario, I'll try that!


Last updated: May 14 2021 at 14:20 UTC