Zulip Chat Archive

Stream: new members

Topic: Inferring fintype for a function


view this post on Zulip Yakov Pechersky (Oct 15 2020 at 21:47):

What's the missing piece here?

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

view this post on Zulip Yakov Pechersky (Oct 15 2020 at 21:49):

Ah:

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

view this post on Zulip Julian Berman (Oct 15 2020 at 21:51):

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

view this post on Zulip Julian Berman (Oct 15 2020 at 21:52):

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

view this post on Zulip Julian Berman (Oct 15 2020 at 21:53):

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


Last updated: May 09 2021 at 20:11 UTC