# Zulip Chat Archive

## Stream: maths

### Topic: set.finite.fintype

#### Kevin Buzzard (Jan 28 2020 at 17:05):

import data.set.finite open set /- From data.set.finite: noncomputable instance finite.fintype {s : set α} (h : finite s) : fintype s := classical.choice h -/ example (α : Type*) (s : set α) (hs : finite s) : fintype s := by apply_instance /- tactic.mk_instance failed to generate instance for fintype ↥s state: α : Type ?, s : set α, hs : finite s ⊢ fintype ↥s -/ noncomputable example (α : Type*) (s : set α) (hs : finite s) : fintype s := by apply_instance -- same error noncomputable theory open_locale classical local attribute [instance, priority 10000] set.finite.fintype example (α : Type*) (s : set α) (hs : finite s) : fintype s := by apply_instance -- same error

The instance `finite s -> fintype s`

-- I can't ever get it to fire. I just changed `instance`

to `def`

in mathlib and recompiled, and it seems to compile fine (I haven't finished yet but it's been running for a while). Should it be a `def`

?

#### Yury G. Kudryashov (Jan 28 2020 at 17:15):

I think it should

#### Reid Barton (Jan 29 2020 at 00:06):

We could detect this with a linter, right? `hs`

is not a type class argument (and `finite`

is not even a class--does this matter?) and nothing depends on `hs`

so there is no way it could ever be inferred, either.

#### Mario Carneiro (Jan 29 2020 at 00:09):

I like the idea of checking this with a linter. It can definitely be done

#### Mario Carneiro (Jan 29 2020 at 00:10):

it does matter that `finite`

is not a class

#### Mario Carneiro (Jan 29 2020 at 00:13):

The simplest way to make the linter work is to create a replica of the instance type and try to prove it by `apply_instance`

#### Mario Carneiro (Jan 29 2020 at 00:15):

this might have false negatives for "transitivity" instances like `foo A B -> foo B C -> foo A C`

(which should be discouraged)

Last updated: May 14 2021 at 19:21 UTC