Inferring fintype for a function

Stream: new members

[Yakov Pechersky]

What's the missing piece here?

example {α β : Type*} [fintype α] [fintype β] : fintype (α → β) := by apply_instance -- doesn't generate one

[Yakov Pechersky]

Ah:

example {α β : Type*} [fintype α] [fintype β] [decidable_eq α] [decidable_eq β] :
  fintype (α → β) := pi.fintype

[Julian Berman]

apply_instance looks like it works too once the equality conditions are there

[Julian Berman]

It looks like the [decidable_eq β] isn't actually needed too

[Julian Berman]

(I don't know what I'm doing, just doing compiler driven development)