Zulip Chat Archive

Stream: new members

Topic: enumerated types are fintypes?


view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Johan Commelin (Mar 06 2020 at 17:14):

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 17:15):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 17:28):

Right but presumably one can do this in meta land?

view this post on Zulip 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