## Stream: new members

### Topic: enumerated types are fintypes?

#### Vaibhav Karve (Mar 06 2020 at 16:55):

If I define an enumerate type α, then there should be a way for me to quickly infer that this is a fintype?
Currently I am writing things like

instance α_fin : fintype α := {elems := {α.a, α.b, α.c, α.d},  complete := λ x, by cases x; simp}


Is there an easier way to do this? Some tactic that can handle this?

#### Kevin Buzzard (Mar 06 2020 at 17:13):

Can a derive handler do this? For enumerated types it is presumably not too hard.

I realise that I currently have no idea how to see what the derive handler can do. Here is an example:

@[derive decidable_eq]
inductive foo
| a : foo
| b : foo


But @[derive fintype] doesn't seem to work (and I don't know how to find out what works nowadays).

#### Johan Commelin (Mar 06 2020 at 17:14):

That's because there is no derive handler for fintypes.

#### Kevin Buzzard (Mar 06 2020 at 17:15):

Did Vaibhav just write one, in some sense, for enumerated types?

#### Johan Commelin (Mar 06 2020 at 17:15):

If A is a fintype, and you write def B := A, then @[derive fintype] will use a generic instance derive handler to get a fintype instance for B. But that machine will not work for your inductive type.

#### Johan Commelin (Mar 06 2020 at 17:17):

Kevin Buzzard said:

Did Vaibhav just write one, in some sense, for enumerated types?

Well, you would need an automated way to determine what elems should be.

#### Kevin Buzzard (Mar 06 2020 at 17:28):

Right but presumably one can do this in meta land?

#### Vaibhav Karve (Mar 06 2020 at 17:34):

Thanks, that's good to know. So for now, I will keep on writing these explicit instances.

Last updated: May 15 2021 at 23:13 UTC