Zulip Chat Archive

Stream: general

Topic: fintype.card


view this post on Zulip Reid Barton (Aug 02 2019 at 19:48):

This works if I comment out the first, unneeded import.

import data.set.finite
import data.fintype

local attribute [instance, priority 1] classical.prop_decidable

-- set_option trace.class_instances true
variables {n : } {H : set (fin n)} (hH : fintype.card H > 3)
-- maximum class-instance resolution depth has been reached ...

view this post on Zulip Reid Barton (Aug 02 2019 at 19:48):

Anyone know what's going on? Or is there a better way to state the hypothesis?

view this post on Zulip Chris Hughes (Aug 02 2019 at 19:54):

Is it decidable_mem_of_fintype and subtype.fintype cycling? That's a guess without Lean in front of me.

view this post on Zulip Reid Barton (Aug 02 2019 at 19:54):

Yeah it looks like it

view this post on Zulip Reid Barton (Aug 02 2019 at 19:56):

At least, decidable_mem_of_fintype is definitely involved

view this post on Zulip Reid Barton (Aug 02 2019 at 19:57):

Can I locally make it not an instance?

view this post on Zulip Reid Barton (Aug 02 2019 at 19:57):

Well I locally gave it priority 0 and that seems to have fixed it


Last updated: May 08 2021 at 09:11 UTC