Zulip Chat Archive

Stream: general

Topic: Type class failure

Chris Hughes (Jul 19 2019 at 14:19):

What's failing here?

import ring_theory.noetherian ring_theory.principal_ideal_domain

example {K : Type*} [discrete_field K] : is_noetherian_ring K := by apply_instance --works
example {K : Type*} [discrete_field K] : is_noetherian K K := by apply_instance --fails

Rob Lewis (Jul 19 2019 at 15:43):

The [fintype M] argument to ring.is_noetherian_of_fintype should be the first instance argument.

Chris Hughes (Jul 19 2019 at 15:52):

Thanks.

Johan Commelin (Jul 22 2019 at 01:13):

I've put your PR on the merge queue. It's sad that this kind of hackery is needed...

Johan Commelin (Jul 22 2019 at 01:14):

I still don't understand how to debug these kinds of things.

Last updated: Dec 20 2023 at 11:08 UTC