enumerated types are fintypes?

Stream: new members

[Vaibhav Karve]

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]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

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]

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]

Right but presumably one can do this in meta land?

[Vaibhav Karve]

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